Theory GyroVectorSpaceTrivial

theory GyroVectorSpaceTrivial
  imports GyroVectorSpace
begin

text ‹Every group is a gyrogroup with identity gyration›
sublocale group_add ⊆ groupGyrogroupoid: gyrogroupoid 0 "(+)"
  by unfold_locales

sublocale group_add ⊆ groupGyrogroup: gyrogroup 0 "(+)" "λ x. - x" "λ u v x. x"
proof
  fix a
  show "0 + a = a"
    by auto
next
  fix a
  show "- a + a = 0"
    by auto
next
  fix a b z
  show "a + (b + z) = a + b + z"
    by (simp add: add_assoc)
next
  fix a b
  show "(λ x. x) = (λ x. x)"
    by auto
next
  fix a b
  show "gyrogroupoid.gyroaut (+) (λx. x)"
    unfolding gyrogroupoid.gyroaut_def
    by (auto simp add: bij_def)
qed

locale gyrocarrier_trivial = gyrocarrier' to_carrier for 
  to_carrier :: "'a::{gyrocommutative_gyrogroup, real_inner, real_normed_algebra_1} ⇒ 'a" + 
  assumes gyr_id: "⋀ u v x. (gyr::'a ⇒ 'a ⇒ 'a ⇒ 'a) u v x = x"
  assumes to_carrier_id: "⋀ x. to_carrier x = x"
  assumes oplus: "⋀ x y::'a . x ⊕ y = x + y"
  assumes ominus: "⋀ x::'a . ⊖ x = - x"

sublocale gyrocarrier_trivial ⊆ gyrocarrier to_carrier
proof
  fix u v a b
  show "gyr u v a ⋅ gyr u v b = a ⋅ b"
    by (simp add: gyr_id)
qed

sublocale gyrocarrier_trivial ⊆ pre_gyrovector_space to_carrier "(*⇩R)"
proof
  fix a::'a
  show "1 *⇩R a = a"
    by auto
next
  fix r1 r2 and a::'a
  show "(r1 + r2) *⇩R a = (r1 *⇩R a) ⊕ (r2 *⇩R a)"
    unfolding oplus
    by (meson scaleR_left_distrib)
next
  fix r1 r2 and a::'a
  show "(r1 * r2) *⇩R a = r1 *⇩R r2 *⇩R a"
    by simp
next
  fix u v a :: 'a and r
  show "gyr u v (r *⇩R a) = r *⇩R gyr u v a"
    unfolding gyr_id
    by simp
next
  fix r1 r2 and v :: 'a
  show "gyr (r1 *⇩R v) (r2 *⇩R v) = id"
    by (auto simp add: gyr_id)
next
  fix r::real and a::'a
  assume "r ≠ 0" "a ≠ 0⇩g"
  show "to_carrier (¦r¦ *⇩R a) /⇩R ⟪(r *⇩R a)⟫ = to_carrier a /⇩R ⟪a⟫"
    by (simp add: ‹r ≠ 0› gyronorm_def to_carrier_id)
qed

sublocale gyrocarrier_trivial ⊆ TG': gyrocarrier_norms_embed' to_carrier
proof
  show "of_real ` norms ⊆ carrier"
    unfolding norms_def carrier_def
    by (simp add: to_carrier_id)
qed

context gyrocarrier_trivial
begin

lemma norms_UNIV:
  shows "norms = UNIV"
  unfolding norms_def
  by (auto, metis eq_abs_iff' gyronorm_def norm_of_real to_carrier_id)

lemma reals_UNIV:
  shows "TG'.reals = of_real ` UNIV"
  unfolding TG'.reals_def norms_UNIV
  using of_carrier to_carrier_id 
  by auto

lemma of_real':
  shows "TG'.of_real' = of_real"
  using TG'.of_real'_def
  using of_carrier to_carrier_id 
  by auto

end

sublocale gyrocarrier_trivial ⊆ TG: gyrocarrier_norms_embed to_carrier "(*⇩R)"
proof
  fix a b
  assume "a ∈ TG'.reals" "b ∈ TG'.reals"
  then show "a ⊕ b ∈ TG'.reals"
    unfolding reals_UNIV oplus
    by (metis Reals_add Reals_def)
next
  fix a
  assume "a ∈ TG'.reals"
  then show "⊖ a ∈ TG'.reals"
    unfolding reals_UNIV ominus
    by force
next
  fix a r
  assume "a ∈ TG'.reals"
  then show "r *⇩R a ∈ TG'.reals"
    unfolding reals_UNIV
    by (metis Reals_def Reals_mult Reals_of_real scaleR_conv_of_real)
qed

sublocale gyrocarrier_trivial ⊆ gyrovector_space_norms_embed "(*⇩R)" to_carrier
proof
  fix r a
  show "⟪(r *⇩R a)⟫ = TG.otimesR ¦r¦ (⟪a⟫)"
    unfolding gyronorm_def TG.otimesR_def of_real'
    by (metis TG'.to_real' UNIV_I norm_scaleR norms_UNIV of_real' of_real_mult scaleR_conv_of_real to_carrier_id)
next
  fix a b
  show "⟪a ⊕ b⟫ ≤ ⟪a⟫ ⊕⇩R (⟪b⟫)"
    by (metis TG'.oplusR_def TG'.to_real' UNIV_I gyronorm_def norm_triangle_ineq norms_UNIV of_real' of_real_add oplus to_carrier_id)    
qed

end