Theory GyroVectorSpaceIsomorphism

theory GyroVectorSpaceIsomorphism
  imports GyroVectorSpace
begin

locale gyrocarrier_isomorphism' =
       gyrocarrier_norms_embed' to_carrier +
       gyrocarrier to_carrier + 
   G:  gyrocarrier_norms_embed' to_carrier'
   for to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner, real_normed_algebra_1}" and
       to_carrier' :: "'c::gyrocommutative_gyrogroup ⇒ 'd::{real_inner, real_normed_algebra_1}"  +
 fixes φ :: "'a ⇒ 'c"
begin

definition φ⇩R :: "real ⇒ real" where 
  "φ⇩R x = G.to_real' (φ (of_real' x))"

end

locale gyrocarrier_isomorphism = gyrocarrier_isomorphism' +
  assumes φbij [simp]:
    "bij φ"
  assumes φplus [simp]:
    "⋀ u v :: 'a. φ (u ⊕ v) = φ u ⊕ φ v"
  assumes φinner_unit:
    "⋀ u v :: 'a. ⟦u ≠ 0⇩g; v ≠ 0⇩g⟧ ⟹
                    inner (to_carrier' (φ u) /⇩R G.gyronorm (φ u)) (to_carrier' (φ v) /⇩R G.gyronorm (φ v)) = 
                    inner (to_carrier u /⇩R gyronorm u) (to_carrier v /⇩R gyronorm v)"
  assumes φ⇩Rgyronorm [simp]:
    "⋀ a. φ⇩R (gyronorm a) = G.gyronorm (φ a)"
begin

lemma φinvφ [simp]:
  shows "φ (inv φ a) = a"
  by (meson φbij bij_inv_eq_iff)

lemma invφφ [simp]:
  shows "(inv φ) (φ a) = a"
  by (metis φbij bij_inv_eq_iff)

lemma φzero [simp]:
  shows "φ 0⇩g = 0⇩g"
  by (metis φplus gyro_left_cancel gyro_right_id)

lemma φminus [simp]:
  shows "φ (⊖ a) = ⊖ (φ a)"
  by (metis φplus φzero gyro_equation_left gyro_left_inv)

lemma invφplus[simp]:
  shows "(inv φ)(a ⊕ b) = inv φ a ⊕ inv φ b"
  by (metis φbij φplus bij_inv_eq_iff)

lemma φgyr [simp]:
  shows "φ (gyr u v a) = gyr (φ u) (φ v) (φ a)"
  by (simp add: gyr_def)

lemma invφgyr [simp]:
  shows "(inv φ) (gyr u v a) = gyr (inv φ u) (inv φ v) (inv φ a)"
  by (metis φbij φgyr bij_inv_eq_iff)

lemma φinner:
  assumes "u ≠ 0⇩g" "v ≠ 0⇩g"
  shows "G.gyroinner (φ u) (φ v) =
         (G.gyronorm (φ u) / gyronorm u) *⇩R (G.gyronorm (φ v) / gyronorm v) *⇩R gyroinner u v"
proof-
  have "φ u ≠ 0⇩g" "φ v ≠ 0⇩g"
    by (metis φbij φzero assms(1) bij_inv_eq_iff)
       (metis φbij φzero assms(2) bij_inv_eq_iff)
  then have "G.gyronorm (φ u) ≠ 0" "G.gyronorm (φ v) ≠ 0"
    using G.norm_zero_iff 
    by blast+
  then have "inner (to_carrier' (φ u)) (to_carrier' (φ v)) = 
        G.gyronorm (φ u) *⇩R G.gyronorm (φ v) *⇩R inner (to_carrier' (φ u) /⇩R G.gyronorm (φ u)) (to_carrier' (φ v) /⇩R G.gyronorm (φ v))"
    by (smt (verit, ccfv_threshold) divideR_right inner_commute inner_scaleR_right real_scaleR_def)
  also have "… = G.gyronorm (φ u) *⇩R G.gyronorm (φ v) *⇩R inner (to_carrier u /⇩R gyronorm u) (to_carrier v /⇩R gyronorm v)"
    using φinner_unit[OF assms]
    by simp
  finally show ?thesis
    unfolding G.gyroinner_def gyroinner_def
    by (simp add: divide_inverse_commute)
qed

lemma gyronorm'gyr:
  shows "G.gyronorm (gyr u v a) = G.gyronorm a"
proof (cases "a = 0⇩g")
  case True
  then show ?thesis
    by (simp add: gyr_id_3)
next
  case False
  then show ?thesis
    by (metis φ⇩Rgyronorm φinvφ invφgyr norm_gyr)
qed

end

sublocale gyrocarrier_isomorphism ⊆ gyrocarrier to_carrier'
proof
  fix u v a b
  show "G.gyroinner (gyr u v a) (gyr u v b) = G.gyroinner a b"
  proof (cases "a = 0⇩g ∨ b = 0⇩g")
    case True
    then show ?thesis
      by (metis G.gyroinner_def G.to_carrier_zero gyr_id_3 inner_zero_left inner_zero_right)
  next
    case False

    let ?Ga = "gyr (inv φ u) (inv φ v) (inv φ a)" and ?Gb = "gyr (inv φ u) (inv φ v) (inv φ b)"

    have "G.gyroinner (gyr u v a) (gyr u v b) = G.gyroinner (φ ?Ga) (φ ?Gb)"
      using invφgyr 
      by simp
    also have "… = (G.gyronorm (φ ?Ga) / ⟪?Ga⟫) *⇩R (G.gyronorm (φ ?Gb) / ⟪?Gb⟫) *⇩R ?Ga ⋅ ?Gb" 
    proof (subst φinner)
      show "gyr (inv φ u) (inv φ v) (inv φ a) ≠ 0⇩g"
        by (metis False φinvφ φzero gyr_id_3 gyr_inj)
    next
      show "gyr (inv φ u) (inv φ v) (inv φ b) ≠ 0⇩g"
        by (metis False φinvφ φzero gyr_id_3 gyr_inj)
    qed simp
    also have "… = (G.gyronorm (φ ?Ga) / ⟪?Ga⟫) *⇩R (G.gyronorm (φ ?Gb) / ⟪?Gb⟫) *⇩R (inv φ a) ⋅ (inv φ b)"
      using inner_gyroauto_invariant
      by presburger
    finally have "G.gyroinner (gyr u v a) (gyr u v b) = (G.gyronorm (gyr u v a) / gyronorm ?Ga) *⇩R (G.gyronorm (gyr u v b) / gyronorm ?Gb) *⇩R (inv φ a) ⋅ (inv φ b)"
      by auto

    moreover

    have "G.gyroinner a b = (G.gyronorm a / ⟪inv φ a⟫) *⇩R (G.gyronorm b / ⟪inv φ b⟫) *⇩R inv φ a ⋅ inv φ b"
      using φinner[of "inv φ a" "inv φ b"] 
      by (metis False φinvφ φzero)

    moreover
    have "⟪gyr (inv φ u) (inv φ v) (inv φ a)⟫ = ⟪inv φ a⟫"
         "⟪gyr (inv φ u) (inv φ v) (inv φ b)⟫ = ⟪inv φ b⟫"
      by (auto simp add: norm_gyr)

    moreover

    have "G.gyronorm (gyr u v a) = G.gyronorm a"
         "G.gyronorm (gyr u v b) = G.gyronorm b"
      using gyronorm'gyr
      by auto
 
    ultimately

    show ?thesis
      by simp
  qed
qed

locale pre_gyrovector_space_isomorphism' = 
    pre_gyrovector_space to_carrier scale + 
    gyrocarrier_norms_embed' to_carrier + 
  GC: gyrocarrier_norms_embed' to_carrier'  
  for to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner, real_normed_algebra_1}" and
      to_carrier' :: "'c::gyrocommutative_gyrogroup ⇒ 'd::{real_inner, real_normed_algebra_1}" and
      scale :: "real ⇒ 'a ⇒ 'a" and 
      scale' :: "real ⇒ 'c ⇒ 'c"  +
  fixes φ :: "'a ⇒ 'c"

sublocale pre_gyrovector_space_isomorphism' ⊆ gyrocarrier_isomorphism'
  ..

locale pre_gyrovector_space_isomorphism = 
   pre_gyrovector_space_isomorphism' +
   gyrocarrier_isomorphism +
   assumes φscale [simp]:
      "⋀ r :: real. ⋀ u :: 'a. φ (scale r u) = scale' r (φ u)"
begin

lemma scale'_1:
  shows "scale' 1 a = a"
  using φscale[of 1 "(inv φ) a"]
  by (simp add: scale_1)

lemma scale'_distrib:
  shows "scale' (r1 + r2) a = scale' r1 a ⊕ scale' r2 a"
  using φscale[symmetric, of "r1 + r2" "(inv φ) a"]
  using scale_distrib
  by auto

lemma scale'_assoc:
  shows "scale' (r1 * r2) a = scale' r1 (scale' r2 a)"
  using φscale[symmetric, of "r1 * r2" "(inv φ) a"]
  using scale_assoc 
  by force

lemma scale'_gyroauto_id:
  shows "gyr (scale' r1 v) (scale' r2 v) = id"
proof
  fix x
  show "gyr (scale' r1 v) (scale' r2 v) x = id x"
    using φscale[symmetric, of r1 "(inv φ) v"] φscale[symmetric, of r2 "(inv φ) v"]
    by (metis φinvφ gyroauto_id id_apply invφφ invφgyr)
qed

lemma scale'_gyroauto_property:
  shows "gyr u v (scale' r a) = scale' r (gyr u v a)"
  using φscale[of r "inv φ (gyr u v a)"]
  using φscale[of r "inv φ a"]
  by (metis φbij bij_inv_eq_iff gyroauto_property invφgyr)

end

locale gyrovector_space_isomorphism' = 
  pre_gyrovector_space_isomorphism + 
  gyrovector_space_norms_embed scale +
  GC: gyrocarrier_norms_embed to_carrier' scale' +
  assumes φreals:
    "φ ` reals = GC.reals"
begin

lemma φ⇩Rnorms:
  assumes "a ∈ norms"
  shows "φ⇩R a ∈ GC.norms"
  using assms
  by (metis GC.bij_betw_to_real' φ⇩R_def φreals bij_betw_iff_bijections bij_reals_norms image_iff)

lemma φof_real'[simp]:
  assumes "a ∈ norms"
  shows "φ (of_real' a) = GC.of_real' (φ⇩R a)"
  using assms
  by (metis GC.of_real' φ⇩R_def φreals bij_betwE bij_reals_norms image_iff)

lemma φgyronorm [simp]:
  shows "φ (of_real' (gyronorm a)) = GC.of_real' (GC.gyronorm (φ a))"
  by simp

lemma φ⇩Rplus [simp]:
  assumes "a ∈ norms" "b ∈ norms"
  shows "φ⇩R (a ⊕⇩R b) = GC.oplusR (φ⇩R a) (φ⇩R b)"
proof-
  have "φ⇩R (a ⊕⇩R b) = GC.to_real' (φ (of_real' a) ⊕ φ (of_real' b))"
    unfolding φ⇩R_def oplusR_def
  proof (subst of_real')
    show "of_real' a ⊕ of_real' b ∈ reals"
      by (meson assms(1) assms(2) bij_betwE bij_reals_norms oplus_reals)
  qed simp
  then show ?thesis
    using assms
    unfolding GC.oplusR_def
    by simp
qed

lemma φ⇩Rplus' [simp]:
  "φ⇩R ((⟪a⟫) ⊕⇩R (⟪b⟫)) = GC.oplusR (φ⇩R (⟪a⟫)) (φ⇩R (⟪b⟫))"
  by (simp add: GC.oplusR_def φ⇩R_def)

lemma φ⇩Rtimes [simp]:
  assumes "a ∈ norms"
  shows "φ⇩R (r ⊗⇩R a) = GC.otimesR r (φ⇩R a)"
proof-
  have "φ⇩R (r ⊗⇩R a) = GC.to_real' (φ (of_real' (to_real' (scale r (of_real' a)))))"
    unfolding φ⇩R_def otimesR_def
    by simp
  also have "… = GC.to_real' (φ (scale r (of_real' a)))"
    using assms
    by (metis bij_betwE bij_reals_norms of_real' otimes_reals)    
  finally show ?thesis
    using assms
    unfolding GC.otimesR_def
    by simp
qed

lemma φ⇩Rtimes' [simp]:
  shows "φ⇩R (r ⊗⇩R (⟪a⟫)) = GC.otimesR r (φ⇩R (⟪a⟫))"
  by (simp add: GC.otimesR_def φ⇩R_def)

lemma φ⇩Rinv [simp]:
  assumes "a ∈ norms"
  shows "φ⇩R (⊖⇩R a) = GC.oinvR (φ⇩R a)"
proof-
  have "φ⇩R (⊖⇩R a) = GC.to_real' (φ (of_real' (to_real' (⊖ (of_real' a)))))"
    unfolding φ⇩R_def oinvR_def
    by simp
  also have "… = GC.to_real' (φ (⊖ (of_real' a)))"
    by (metis assms bij_betwE bij_reals_norms of_real' oinv_reals)
  finally show ?thesis
    using assms
    unfolding GC.oinvR_def
    by simp
qed

lemma φ⇩Rinv' [simp]:
  "φ⇩R (⊖⇩R (⟪a⟫)) = GC.oinvR (φ⇩R (⟪a⟫))"
  by (simp add: φ⇩R_def GC.oinvR_def)


lemma scale'_prop1':
  assumes "u ≠ 0⇩g" "r ≠ 0"
  shows "to_carrier' (φ (scale ¦r¦ u)) /⇩R GC.gyronorm (φ (scale ¦r¦ u)) = 
         (to_carrier' (φ u) /⇩R GC.gyronorm (φ u))" (is "?a = ?b")
proof-
  have "⟪scale r u⟫ = ⟪scale (abs r) u⟫"
    using homogeneity by force

  have "inner ?b ?a =
        inner (to_carrier u /⇩R ⟪u⟫) (to_carrier (scale ¦r¦ u) /⇩R ⟪scale ¦r¦ u⟫)"
    using φinner_unit[where u=u and v="scale (abs r) u"] 
    by fastforce
  also have "… = inner (to_carrier u /⇩R ⟪u⟫) (to_carrier u /⇩R ⟪u⟫)"
    using scale_prop1[of r u] ‹u ≠ 0⇩g› ‹r ≠ 0› ‹⟪scale r u⟫ = ⟪scale (abs r) u⟫›
    by simp
  finally have "inner ?b ?a = 1"
    by (smt (verit, ccfv_threshold) φinner_unit assms(1) gyronorm_def inverse_nonnegative_iff_nonnegative inverse_nonzero_iff_nonzero left_inverse norm_eq norm_eq_1 norm_le_zero_iff norm_scaleR norm_zero_iff scaleR_eq_0_iff to_carrier_zero_iff)
    
  show ?thesis
  proof (rule inner_eq_1)
    show "inner ?a ?b = 1"
      using ‹inner ?b ?a = 1›
      by (simp add: inner_commute)
  next
    show "norm ?a = 1"
      by (smt (verit, ccfv_threshold) φinner_unit assms(1) assms(2) gyronorm_def scale_prop1 inverse_nonnegative_iff_nonnegative inverse_nonzero_iff_nonzero left_inverse local.norm_zero norm_eq norm_ge_zero norm_scaleR norm_zero_iff scaleR_eq_0_iff to_carrier_zero_iff)
  next
    show "norm ?b = 1"
      using GC.norm_zero_iff φzero assms(1) GC.gyronorm_def invφφ inverse_negative_iff_negative left_inverse norm_not_less_zero norm_scaleR
      by (smt (verit, del_insts))
  qed
qed 

lemma scale'_prop1:
  assumes "a ≠ 0⇩g" "r ≠ 0"
  shows "to_carrier' (scale' ¦r¦ a) /⇩R GC.gyronorm (scale' r a) = to_carrier' a /⇩R GC.gyronorm a"
proof-
  from assms have *: "inv φ a ≠ 0⇩g" "r ≠ 0"
    by (metis φinvφ φzero, simp)
  show ?thesis
    using scale'_prop1'[OF *]
    by (metis φ⇩Rgyronorm φinvφ φscale abs_idempotent homogeneity)
qed

lemma scale'_homogeneity:
  shows "GC.gyronorm (scale' r a) = GC.otimesR ¦r¦ (GC.gyronorm a)"
proof-
  have "GC.gyronorm (scale' r a) = GC.gyronorm (φ (scale r (inv φ a)))"
    using φscale[of r "inv φ a"]
    by simp
  also have "… = φ⇩R (gyronorm (scale r (inv φ a)))"
    by simp
  also have "… = φ⇩R (¦r¦ ⊗⇩R (⟪inv φ a⟫))"
    using homogeneity
    by simp
  also have "… =  φ⇩R (to_real' (scale ¦r¦ (of_real' (⟪inv φ a⟫))))"
    unfolding otimesR_def
    by simp
  also have "… = GC.to_real' (φ (scale ¦r¦ (of_real' (gyronorm (inv φ a)))))"
    using GC.otimesR_def φ⇩Rtimes otimesR_def
    by force
  also have "… = GC.to_real' (scale' ¦r¦ (φ (of_real' (gyronorm (inv φ a)))))"
    using φscale
    by simp
  also have "… = GC.to_real' (scale' ¦r¦ (GC.of_real' (GC.gyronorm (φ (inv φ a)))))"
    by (subst φgyronorm, simp)
  finally
  show "GC.gyronorm (scale' r a) = GC.otimesR ¦r¦ (GC.gyronorm a)"
    unfolding GC.otimesR_def
    by simp
qed

end

sublocale gyrovector_space_isomorphism' ⊆ GV: pre_gyrovector_space to_carrier' scale'
  by (meson gyrocarrier_axioms scale'_prop1  pre_gyrovector_space.intro pre_gyrovector_space_axioms.intro scale'_1 scale'_assoc scale'_distrib scale'_gyroauto_id scale'_gyroauto_property)

locale gyrovector_space_isomorphism = 
  gyrovector_space_isomorphism' + 
  assumes φ⇩Rmono:
    "⋀ a b. ⟦a ∈ norms; b ∈ norms; 0 ≤ a; a ≤ b⟧ ⟹ φ⇩R a ≤ φ⇩R b" 
begin

lemma scale'_triangle:
  shows  "GC.gyronorm (a ⊕ b) ≤ GC.oplusR (GC.gyronorm a) (GC.gyronorm b)"
proof-
  have "GC.gyronorm (a ⊕ b) = φ⇩R (⟪inv φ a ⊕ inv φ b⟫)"
    by simp
  moreover
  have "GC.oplusR (GC.gyronorm a) (GC.gyronorm b) = φ⇩R ((⟪inv φ a⟫) ⊕⇩R (⟪inv φ b⟫))"
    by simp
  moreover
  have "φ⇩R (⟪inv φ a ⊕ inv φ b⟫) ≤ φ⇩R ((⟪inv φ a⟫) ⊕⇩R (⟪inv φ b⟫))"
  proof (rule φ⇩Rmono)
    show "⟪inv φ a ⊕ inv φ b⟫ ∈ norms"
      unfolding norms_def
      by auto
  next
    show "⟪inv φ a⟫ ⊕⇩R (⟪inv φ b⟫) ∈ norms"
    proof (rule oplusR_norms)
      show "⟪inv φ a⟫ ∈ norms" "⟪inv φ b⟫ ∈ norms"
        unfolding norms_def
        by auto
    qed
  next
    show "0 ≤ ⟪inv φ a ⊕ inv φ b⟫"
      by (simp add: gyronorm_def)
  next
    show "⟪inv φ a ⊕ inv φ b⟫ ≤ (⟪inv φ a⟫) ⊕⇩R (⟪inv φ b⟫)"
      by (simp add: gyrotriangle)
  qed
  ultimately
  show  "GC.gyronorm (a ⊕ b) ≤ GC.oplusR (GC.gyronorm a) (GC.gyronorm b)"
    by simp
qed

end

sublocale gyrovector_space_isomorphism ⊆ gyrovector_space_norms_embed scale' to_carrier'
  by (meson GC.gyrocarrier_norms_embed_axioms GV.pre_gyrovector_space_axioms gyrocarrier_axioms gyrovector_space_isomorphism.scale'_triangle gyrovector_space_isomorphism_axioms gyrovector_space_norms_embed_axioms.intro gyrovector_space_norms_embed_def scale'_homogeneity)

(* ------------------------------------------------------------ *)

locale gyrocarrier_isomorphism_norms_embed' = gyrovector_space_norms_embed scale to_carrier + 
             GC: gyrocarrier_norms_embed' to_carrier'
  for to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner, real_normed_algebra_1}" and
      to_carrier' :: "'c::gyrocommutative_gyrogroup ⇒ 'd::{real_inner, real_normed_algebra_1}" and
      scale :: "real ⇒ 'a ⇒ 'a" + 
  fixes scale' :: "real ⇒ 'c ⇒ 'c" 
  fixes φ :: "'a ⇒ 'c"
begin

definition φ⇩R :: "real ⇒ real" where 
  "φ⇩R x = GC.to_real' (φ (of_real' x))"

end

locale gyrocarrier_isomorphism_norms_embed = gyrocarrier_isomorphism_norms_embed' +
  assumes φbij:
    "bij φ"
  assumes φplus [simp]:
    "⋀ u v :: 'a. φ (u ⊕ v) = φ u ⊕ φ v"
  assumes φscale [simp]:
    "⋀ r :: real. ⋀ u :: 'a. φ (scale r u) = scale' r (φ u)"
  assumes φreals:
    "φ ` reals = GC.reals"
  assumes φ⇩Rgyronorm [simp]:
    "⋀ a. φ⇩R (gyronorm a) = GC.gyronorm (φ a)"
  assumes GCoinvRminus:
    "⋀ a. a ∈ GC.norms ⟹ GC.oinvR a = -a"
begin

lemma φinvφ [simp]:
  shows "φ (inv φ a) = a"
  by (meson φbij bij_inv_eq_iff)

lemma φzero [simp]:
  shows "φ 0⇩g = 0⇩g"
  by (metis φplus gyro_left_cancel gyro_right_id)

lemma φminus [simp]:
  shows "φ (⊖ a) = ⊖ (φ a)"
  by (metis φplus φzero gyro_equation_left gyro_left_inv)

lemma φgyronorm [simp]:
  shows "φ (of_real' (gyronorm a)) = GC.of_real' (GC.gyronorm (φ a))"
  by (metis (no_types, opaque_lifting) GC.of_real' φ⇩R_def φ⇩Rgyronorm φreals bij_betwE bij_reals_norms image_eqI norm_in_norms)

lemma φ⇩Rinv' [simp]:
  "φ⇩R (⊖⇩R (⟪a⟫)) = GC.oinvR (φ⇩R (⟪a⟫))"
  by (simp add: GC.oinvR_def φ⇩R_def)
end

sublocale gyrocarrier_isomorphism_norms_embed ⊆ GV': gyrocarrier_norms_embed to_carrier' scale'
proof
  fix a b
  assume "a ∈ GC.reals" "b ∈ GC.reals"
  then obtain x y where 
    "a = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ∨ a = GC.of_real' (- φ⇩R (⟪inv φ x⟫))" 
    "b = GC.of_real' (φ⇩R (⟪inv φ y⟫)) ∨ b = GC.of_real' (- φ⇩R (⟪inv φ y⟫))"
    unfolding GC.reals_def GC.norms_def GC.of_real'_def
    by fastforce
  then have "a ⊕ b = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (φ⇩R (⟪inv φ y⟫)) ∨
             a ⊕ b = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (- φ⇩R (⟪inv φ y⟫)) ∨ 
             a ⊕ b = GC.of_real' (- φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (- φ⇩R (⟪inv φ y⟫)) ∨ 
             a ⊕ b = GC.of_real' (- φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (φ⇩R (⟪inv φ y⟫))"
    by auto
  then have "a ⊕ b = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (φ⇩R (⟪inv φ y⟫)) ∨
             a ⊕ b = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ⊕ GC.of_real' (φ⇩R (⊖⇩R (⟪inv φ y⟫))) ∨ 
             a ⊕ b = GC.of_real' (φ⇩R (⊖⇩R (⟪inv φ x⟫))) ⊕ GC.of_real' (φ⇩R (⊖⇩R ((⟪inv φ y⟫)))) ∨ 
             a ⊕ b = GC.of_real' (φ⇩R (⊖⇩R (⟪inv φ x⟫))) ⊕ GC.of_real' (φ⇩R (⟪inv φ y⟫))"
    by (simp add: GCoinvRminus)
  then show "a ⊕ b ∈ GC.reals"
    by (smt (verit, del_insts) ‹a ∈ GC.reals› ‹b ∈ GC.reals› φplus φreals image_iff oplus_reals)
next
  fix a
  assume "a ∈ GC.reals"
  then obtain x where 
    "a = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ∨ a = GC.of_real' (- φ⇩R (⟪inv φ x⟫))" 
    unfolding GC.reals_def GC.norms_def GC.of_real'_def
    by fastforce
  then have "⊖ a = ⊖ (GC.of_real' (φ⇩R (⟪inv φ x⟫))) ∨
             ⊖ a = ⊖ (GC.of_real' (- φ⇩R (⟪inv φ x⟫)))"
    by auto
  then have "⊖ a = ⊖ (GC.of_real' (φ⇩R (⟪inv φ x⟫))) ∨
             ⊖ a = ⊖ (GC.of_real' (φ⇩R (⊖⇩R (⟪inv φ x⟫))))"
    by (simp add: GCoinvRminus)
  then show "⊖ a ∈ GC.reals"
    by (metis (no_types, opaque_lifting) ‹a ∈ GC.reals› φminus φreals image_iff oinv_reals)
next
  fix a r
  assume "a ∈ GC.reals"
  then obtain x where 
    "a = GC.of_real' (φ⇩R (⟪inv φ x⟫)) ∨ a = GC.of_real' (- φ⇩R (⟪inv φ x⟫))" 
    unfolding GC.reals_def GC.norms_def GC.of_real'_def
    by fastforce
  then have "scale' r a = scale' r (GC.of_real' (φ⇩R (⟪inv φ x⟫))) ∨
             scale' r a = scale' r (GC.of_real' (- φ⇩R (⟪inv φ x⟫)))"
    by auto
  then have "scale' r a = scale' r (GC.of_real' (φ⇩R (⟪inv φ x⟫))) ∨
             scale' r a = scale' r (GC.of_real' (φ⇩R (⊖⇩R (⟪inv φ x⟫))))"
    by (simp add: GCoinvRminus)
  then show "scale' r a ∈ GC.reals"
    by (smt (verit, best) ‹a ∈ GC.reals› φreals φscale image_iff otimes_reals)
qed

end