Theory GyroVectorSpace

theory GyroVectorSpace
  imports GyroGroup "HOL-Analysis.Inner_Product" HOL.Real_Vector_Spaces More_Real_Vector
begin

locale gyrocarrier' = 
  fixes to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner}"
  assumes inj_to_carrier [simp]: "inj to_carrier"
  assumes to_carrier_zero [simp]: "to_carrier 0⇩g = 0"
begin

definition carrier :: "'b set" where
  "carrier = to_carrier ` UNIV"

lemma bij_betw_to_carrier:
  shows "bij_betw to_carrier UNIV carrier"
  by (simp add: bij_betw_def carrier_def)

definition of_carrier :: "'b ⇒ 'a" where
  "of_carrier = inv to_carrier"

lemma bij_betw_of_carrier:
  shows "bij_betw of_carrier carrier UNIV"
  by (simp add: carrier_def inj_imp_bij_betw_inv of_carrier_def)

lemma inj_on_of_carrier [simp]: 
  shows "inj_on of_carrier carrier"
  using bij_betw_imp_inj_on bij_betw_of_carrier 
  by auto

lemma to_carrier [simp]:  
  shows "⋀ b. b ∈ carrier ⟹ to_carrier (of_carrier b) = b"
  by (simp add: carrier_def f_inv_into_f of_carrier_def)

lemma of_carrier [simp]: 
  shows "⋀ a. of_carrier (to_carrier a) = a"
  by (simp add: of_carrier_def)

lemma of_carrier_zero [simp]:
  shows "of_carrier 0 = 0⇩g"
  by (simp add: inv_f_eq of_carrier_def)

lemma to_carrier_zero_iff:
  assumes "to_carrier a = 0"
  shows "a = 0⇩g"
  using assms
  by (metis of_carrier to_carrier_zero)

definition gyronorm :: "'a ⇒ real" ("⟪_⟫" [100] 100) where
  "⟪a⟫ = norm (to_carrier a)"

definition gyroinner :: "'a ⇒ 'a ⇒ real" (infixl "⋅" 100) where
  "a ⋅ b = inner (to_carrier a) (to_carrier b)"

lemma norm_inner: "⟪a⟫ = sqrt (a ⋅ a)"
  using gyroinner_def gyronorm_def norm_eq_sqrt_inner by auto

lemma norm_zero:
  shows "⟪0⇩g⟫ = 0"
  by (simp add: gyronorm_def)

lemma norm_zero_iff:
  assumes "⟪a⟫ = 0"
  shows "a = 0⇩g"
  using assms
  by (simp add: gyronorm_def to_carrier_zero_iff)

definition norms :: "real set" where 
 "norms = {x. ∃ a. x = ⟪a⟫} ∪ {x. ∃ a. x = - ⟪a⟫}"

lemma norm_in_norms [simp]:
  shows "⟪a⟫ ∈ norms"
  by (auto simp add: norms_def)

lemma minus_norm_in_norms [simp]:
  shows "- ⟪a⟫ ∈ norms"
  by (auto simp add: norms_def)

end

locale gyrocarrier = gyrocarrier' +  
  assumes inner_gyroauto_invariant: "⋀ u v a b. (gyr u v a) ⋅ (gyr u v b) = a ⋅ b"
begin

lemma norm_gyr: "⟪gyr u v a⟫ = ⟪a⟫"
  by (metis inner_gyroauto_invariant norm_inner)

end

locale pre_gyrovector_space = gyrocarrier + 
  fixes scale :: "real ⇒ 'a ⇒ 'a" (infixl "⊗" 105) 
  assumes scale_1:
    "⋀ a :: 'a.
         1 ⊗ a = a"
  assumes scale_distrib: 
    "⋀ (r1 :: real) (r2 :: real) (a :: 'a). 
         (r1 + r2) ⊗ a = r1 ⊗ a ⊕ r2 ⊗ a"
  assumes scale_assoc: 
    "⋀ (r1 :: real) (r2 :: real) (a :: 'a). 
         (r1 * r2) ⊗ a = r1 ⊗ (r2 ⊗ a)"
  assumes scale_prop1: 
    "⋀ (r :: real) (a :: 'a). 
         ⟦r ≠ 0; a ≠ 0⇩g⟧ ⟹ to_carrier (¦r¦ ⊗ a) /⇩R ⟪r ⊗ a⟫ = to_carrier a /⇩R ⟪a⟫" 
  assumes gyroauto_property: 
    "⋀ (u :: 'a) (v :: 'a) (r :: real) (a :: 'a). 
         gyr u v (r ⊗ a) = r ⊗ (gyr u v a)"
  assumes gyroauto_id:
    "⋀ (r1 :: real) (r2 :: real) (v :: 'a). 
         gyr (r1 ⊗ v) (r2 ⊗ v) = id"
begin

lemma scale_minus1: 
  shows "(-1) ⊗ a = ⊖ a"
  by (metis add.right_inverse add_cancel_right_left gyrogroup_class.gyro_left_cancel' gyrogroup_class.gyro_right_id scale_1 scale_distrib)

lemma minus_norm: 
  shows "⟪⊖a⟫ = ⟪a⟫"
  by (smt (verit, best) gyro_inv_id of_carrier scale_minus1 inverse_eq_iff_eq of_carrier_zero scaleR_cancel_right scale_1 scale_prop1)

text ‹(6.3)›
lemma scale_minus: 
  shows "(-r) ⊗ a = ⊖ (r ⊗ a)"
  by (metis minus_mult_commute mult_1 scale_assoc scale_minus1)

lemma scale_minus': 
  shows "k ⊗ (⊖ a) = ⊖ (k ⊗ a)"
  by (metis mult.commute scale_assoc scale_minus1)

lemma zero_otimes [simp]: 
  shows "0 ⊗ x = 0⇩g"
  by (metis add.right_inverse gyro_rigth_inv scale_distrib scale_minus)

lemma times_zero [simp]: 
  shows "t ⊗ 0⇩g = 0⇩g"
  by (metis mult_zero_right scale_assoc zero_otimes)

text ‹Theorem 6.4 (6.4)›
lemma monodistributive:
  shows "r ⊗ (r1 ⊗ a ⊕ r2 ⊗ a) = r ⊗ (r1 ⊗ a) ⊕ r ⊗ (r2 ⊗ a)"
  by (metis ring_class.ring_distribs(1) scale_assoc scale_distrib)

lemma times2: "2 ⊗ a = a ⊕ a"
  by (metis mult_2_right scale_1 scale_assoc scale_distrib)

lemma twosum: "2 ⊗ (a ⊕ b) = a ⊕ (2 ⊗ b ⊕ a)"
proof-
  have "a ⊕ (2 ⊗ b ⊕ a) = a ⊕ ((b ⊕ b) ⊕ a)"
    by (simp add: times2)
  also have "... = a ⊕ (b ⊕ (b ⊕ gyr b b a))"
    by (simp add: gyro_right_assoc)
  also have "... = a ⊕ (b ⊕ (b ⊕ a))"
    by simp
  also have "... = (a ⊕ b) ⊕ gyr a b (b ⊕ a)"
    using gyro_left_assoc by blast
  also have "... = (a ⊕ b) ⊕ (a ⊕ b)"
    by (metis gyro_commute)
  finally show ?thesis
    by (metis times2)
qed

definition gyrodistance :: "'a ⇒ 'a ⇒ real" ("d⇩⊕") where 
  "d⇩⊕ a b = ⟪⊖ a ⊕ b⟫"

lemma "d⇩⊕ a b = ⟪b ⊖⇩b a⟫"
  by (metis gyrodistance_def gyrogroup_class.gyrominus_def gyro_commute norm_gyr)

lemma gyrodistance_metric_nonneg: 
  shows "d⇩⊕ a b ≥ 0"
  by (simp add: gyrodistance_def gyronorm_def)

lemma gyrodistance_metric_zero_iff:
  shows "d⇩⊕ a b = 0 ⟷ a = b"
  unfolding gyrodistance_def gyronorm_def
  by (metis gyrogroup_class.gyro_left_cancel' gyrogroup_class.gyro_right_id gyronorm_def norm_zero_iff real_normed_vector_class.norm_zero to_carrier_zero)

lemma gyrodistance_metric_sym:
  shows "d⇩⊕ a b = d⇩⊕ b a"
  by (metis gyrodistance_def gyrogroup_class.gyro_inv_idem gyrogroup_class.gyrominus_def gyrogroup_class.gyroplus_inv minus_norm norm_gyr)

lemma equation_solving:
  assumes "x ⊕ y = a" "⊖ x ⊕ y = b"
  shows "x = (1/2) ⊗ (a ⊖⇩c⇩b b) ∧ y = (1/2) ⊗ (a ⊖⇩c⇩b b) ⊕ b"
proof-
  have "y = x ⊕ b"
    using assms(2) gyro_equation_right by auto
  then have "a = x ⊕ (x ⊕ b)"
    using assms(1) by auto
  then have "a = (2 ⊗ x) ⊕ b"
    by (simp add: gyro_left_assoc times2)
  then have "x = (1/2) ⊗ (a ⊖⇩c⇩b b)"
    by (smt (verit) gyro_equation_left nonzero_eq_divide_eq scale_1 scale_assoc)
  then show ?thesis
    using ‹y = x ⊕ b›
    by simp
qed

lemma double_plus: "(2 ⊗ a) ⊕ b = a ⊕ (a ⊕ b)"
 by (simp add: gyro_left_assoc times2)

lemma I6_33:
  shows "(1/2) ⊗ (a ⊖⇩c⇩b b) = (-1/2) ⊗ (b ⊖⇩c⇩b a)"
  by (metis (no_types, opaque_lifting) div_by_1 divide_divide_eq_right divide_minus1 gyrogroup_class.gyro_equation_left gyrogroup_class.gyro_left_cancel' scale_assoc scale_minus1 times_divide_eq_left)

lemma I6_34:
  shows "(1/2) ⊗ (a ⊖⇩c⇩b b) ⊕ b = (1/2) ⊗ (b ⊖⇩c⇩b a) ⊕ a"
  by (smt (verit, ccfv_threshold) I6_33 cogyro_right_cancel' double_plus gyro_left_cancel' mult.commute nonzero_eq_divide_eq scale_1 scale_assoc scale_minus1)

lemma I6_35:
  shows "gyr b a = gyr b ((1/2) ⊗ (a ⊖⇩c⇩b b) ⊕ b) ∘ (gyr ((1/2) ⊗ (a ⊖⇩c⇩b b) ⊕ b) a)"
  by (metis (no_types, lifting) I6_33 I6_34 divide_minus_left gyr_master_misc2' gyr_misc_2 gyr_right_loop gyro_commute gyro_translate_commute scale_minus)

lemma double_half: 
  shows "2 ⊗ ((1 / 2) ⊗ a) = a"
  by (metis field_sum_of_halves mult.commute mult_2_right scale_1 scale_assoc)

lemma I6_38:
  shows "a ⊕ (1/2) ⊗ (⊖ a ⊕⇩c b) = (1/2) ⊗ (a ⊕ b)"
proof -
  have "⋀r r' a. r ⊗ (r' ⊗ a) = r' ⊗ (r ⊗ a)"
    by (metis (full_types) mult.commute scale_assoc)
  then show ?thesis
    using double_half 
    by (smt (z3) gyrogroup_class.cogyro_commute_iff_gyrocommute gyrogroup_class.cogyro_right_cancel' gyrogroup_class.cogyrominus_def gyro_commute twosum)
qed

lemma I6_39:
  shows "a ⊕ (1/2) ⊗ (⊖ a ⊕ b) = (1/2) ⊗ (a ⊕⇩c b)"
  by (metis I6_38 gyro_equation_right gyro_inv_idem)

lemma I6_40:
  shows "gyr ((r + s) ⊗ a) b x = gyr (r⊗a) (s⊗a ⊕ b) (gyr (s⊗a) b x)"
  by (metis (mono_tags, opaque_lifting) comp_eq_elim gyroauto_id id_def gyr_nested_1 scale_distrib)

(* ---------------------------------------------------------------------------- *)
definition collinear :: "'a => 'a => 'a => bool" where
  "collinear x y z ⟷ (y = z ∨ (∃t::real. (x = y ⊕ t ⊗ (⊖ y ⊕ z))))"

lemma collinear_aab:
  shows "collinear a a b"
  by (metis collinear_def gyro_right_id gyro_rigth_inv scale_distrib scale_minus)

lemma collinear_bab:
  shows "collinear b a b"
  by (metis collinear_def gyro_equation_right scale_1)

lemma T6_20:
  assumes "collinear p1 a b" "collinear p2 a b" "a ≠ b" "p1 ≠ p2"
  shows "∀x. (collinear x p1 p2 ⟶ collinear x a b)"
proof safe
  obtain t1 where t1: "p1 = a ⊕ t1 ⊗ (⊖ a ⊕ b)"
    using ‹collinear p1 a b› ‹a ≠ b› collinear_def 
    by auto
  obtain t2 where t2: "p2 = a ⊕ t2 ⊗ (⊖ a ⊕ b)"
    using ‹collinear p2 a b› ‹a ≠ b› collinear_def
    by blast

  fix x
  assume "collinear x p1 p2"
  show "collinear x a b"
  proof-
    obtain t where t: "x = p1 ⊕ t ⊗ (⊖ p1 ⊕ p2)"
      using ‹collinear x p1 p2› ‹p1 ≠ p2› collinear_def 
      by blast
    have "x = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ t ⊗ (⊖ (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ (a ⊕ t2 ⊗ (⊖ a ⊕ b)))"
      using t1 t2 t
      by simp
    then have "x = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ t ⊗ gyr a (t1 ⊗ (⊖ a ⊕ b)) ((-t1 + t2) ⊗ (⊖ a ⊕ b))"
      by (smt (verit, best) gyr_def scale_distrib)
    then have "x = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ gyr a (t1 ⊗ (⊖ a ⊕ b)) ((t*(-t1 + t2)) ⊗ (⊖ a ⊕ b))"
      using gyroauto_property scale_assoc by presburger
    then have "x = a ⊕ (t1 ⊗ (⊖ a ⊕ b) ⊕ ((t*(-t1 + t2)) ⊗ (⊖ a ⊕ b)))"
      by (simp add: gyro_left_assoc)
    then  have "x = a ⊕ (t1 + t*(-t1 + t2)) ⊗ (⊖ a ⊕ b)"
      by (simp add: scale_distrib)
    then show ?thesis  
      using collinear_def by blast
  qed
qed

lemma T6_20_1:
  assumes "collinear p1 a b" "collinear p2 a b" "p1 ≠ p2" "a ≠ b"
  shows "∀x. (collinear x a b ⟶ collinear x p1 p2)"
proof safe
  obtain t1 where t1: "p1 = a ⊕ t1 ⊗ (⊖ a ⊕ b)"
    using ‹collinear p1 a b› ‹a ≠ b› collinear_def 
    by auto
  obtain t3 where t3: "p2 = a ⊕ t3 ⊗ (⊖ a ⊕ b)"
    using ‹collinear p2 a b› ‹a ≠ b› collinear_def
    by blast

  fix x
  assume "collinear x a b"
  show "collinear x p1 p2" 
  proof-
    obtain t2 where "x = a ⊕ t2 ⊗ (⊖ a ⊕ b)"
      using ‹collinear x a b› ‹a ≠ b› collinear_def
      by blast
    show ?thesis
    proof (cases "t1 = t3")
      case True
      then show ?thesis
        using t1 t3 ‹p1 ≠ p2›
        by blast
    next
      case False
      then obtain t where t: "t = (t2-t1)/(t3-t1)" 
        by simp
      have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ t ⊗ (⊖ (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ ( a ⊕ t3 ⊗ (⊖ a ⊕ b)))"
        using t1 t3 by blast
      then have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ t ⊗ gyr a (t1 ⊗ (⊖ a ⊕ b)) (t1 ⊗ (⊖  (⊖ a ⊕ b)) ⊕ t3 ⊗ (⊖ a ⊕ b))"
        by (metis (no_types, lifting) gyro_translation_2a mult.commute scale_assoc scale_minus1)
      then have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = (a ⊕ t1 ⊗ (⊖ a ⊕ b)) ⊕ gyr a (t1 ⊗ (⊖ a ⊕ b)) (((-t1+t3)*t) ⊗ (⊖ a ⊕ b) )"
        by (metis (no_types, opaque_lifting) gyroauto_property minus_mult_commute mult.commute mult.right_neutral scale_assoc scale_distrib scale_minus1)
      then have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = a ⊕ (t1 ⊗ (⊖ a ⊕ b) ⊕ ((-t1+t3)*t) ⊗ (⊖ a ⊕ b)) "
        using gyro_left_assoc by metis
      then have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = a ⊕ (t1 + (-t1+t3)*t) ⊗ ((⊖ a ⊕ b))"
        using scale_distrib by presburger
      moreover have "t1 + (-t1+t3)*t = t2"
        using ‹t1 ≠ t3› t
        by simp
      ultimately
      have "p1 ⊕ t ⊗ (⊖ p1 ⊕ p2) = a ⊕ t2 ⊗ (⊖ a ⊕ b)"
        by blast
      then show ?thesis
        using ‹x = a ⊕ t2 ⊗ (⊖ a ⊕ b)› 
        unfolding collinear_def
        by metis
    qed
  qed
qed

lemma collinear_sym1:
  assumes "collinear a b c"
  shows "collinear b a c"
  using T6_20_1 assms collinear_aab collinear_bab collinear_def by blast

lemma collinear_sym2:
  assumes "collinear a b c"
  shows "collinear a c b"
  by (metis T6_20 assms collinear_aab collinear_bab)

lemma collinear_transitive:
  assumes "collinear a b c" "collinear d b c" "b ≠ c"
  shows "collinear a d b" 
  by (metis T6_20 assms(1) assms(2) assms(3) collinear_bab collinear_sym1 collinear_sym2)

lemma collinear_translate':
  shows "x = u ⊕ t ⊗ (⊖ u ⊕ v) ⟷ 
        (⊖ a ⊕ x) = (⊖ a ⊕ u) ⊕ t ⊗ (⊖ (⊖ a ⊕ u) ⊕ (⊖ a ⊕ v))"
  by (metis (no_types, lifting) gyr_misc_2 gyro_right_assoc gyro_translation_2a gyroauto_property oplus_ominus_cancel)

definition translate where
  "translate a x = ⊖ a ⊕ x"

lemma collinear_translate:
  shows "collinear u v w ⟷ collinear (translate a u) (translate a v) (translate a w)"
  unfolding collinear_def translate_def
  by (metis collinear_translate' gyro_left_cancel')

definition gyroline :: "'a ⇒ 'a ⇒ 'a set" where
  "gyroline a b = {x. collinear x a b}"

definition between :: "'a => 'a => 'a => bool" where
  "between x y z ⟷ (∃t::real. 0 ≤ t ∧ t ≤ 1 ∧ y = x ⊕ t ⊗ (⊖ x ⊕ z))"

lemma between_xxy [simp]:
  shows "between x x y"
  unfolding between_def by force

lemma between_xyy [simp]:
  shows "between x y y"
  unfolding between_def
  by (rule exI [where x=1]) (simp add: scale_1)

lemma between_xyx:
  assumes "between x y x"
  shows "y = x"
  using assms
  unfolding between_def
  by auto

lemma between_translate:
  shows "between u v w ⟷ between (translate a u) (translate a v) (translate a w)"
  unfolding between_def translate_def
  using collinear_translate' 
  by auto

definition distance where
  "distance u v = ⟪⊖ u ⊕ v⟫"

lemma distance_translate:
  shows "distance u v = distance (translate a u) (translate a v)"
  unfolding distance_def translate_def
  using gyro_translation_2a norm_gyr 
  by metis

end

locale gyrocarrier_norms_embed' = gyrocarrier' to_carrier 
  for to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner, real_normed_algebra_1}" +
  assumes norms_carrier: "of_real ` norms ⊆ carrier"
begin

definition of_real' :: "real ⇒ 'a" where
  "of_real' = of_carrier ∘ of_real"

definition reals :: "'a set" where
  "reals = of_carrier ` of_real ` norms"

lemma bij_reals_norms:
  shows "bij_betw of_real' norms reals"
  unfolding of_real'_def
  by (metis bij_betw_def comp_inj_on_iff dual_order.eq_iff image_comp inj_image_eq_iff inj_of_real inj_on_of_carrier norms_carrier reals_def subset_image_inj inj_on_subset)

lemma inj_on_of_real':
  shows "inj_on of_real' norms"
  using bij_betw_imp_inj_on bij_reals_norms
  by blast

definition to_real :: "'b ⇒ real" where 
  "to_real = the_inv_into norms of_real"

lemma to_real [simp]:
  assumes "x ∈ norms"
  shows "to_real (of_real x) = x"
  using assms
  by (metis inj_on_imageI2 inj_on_of_real' of_real'_def the_inv_into_f_f to_real_def)

lemma of_real [simp]:
  assumes "x ∈ of_real ` norms"
  shows "of_real (to_real x) = x"
  using assms
  using to_real
  by force

definition to_real' :: "'a ⇒ real" where 
  "to_real' = to_real ∘ to_carrier"

lemma bij_betw_to_real':
  "bij_betw to_real' reals norms"
  by (smt (verit, best) bij_betw_cong bij_betw_the_inv_into bij_reals_norms comp_apply f_the_inv_into_f to_carrier image_eqI in_mono inj_on_imageI inj_on_imageI2 inj_on_of_real' norms_carrier of_real'_def reals_def the_inv_into_comp the_inv_into_onto to_real'_def to_real_def)

lemma to_real' [simp]: 
  assumes "x ∈ norms"
  shows "to_real' (of_real' x) = x"
  using assms
  using norms_carrier of_real'_def to_real'_def 
  by auto

lemma of_real' [simp]:
  assumes "x ∈ reals"
  shows "of_real' (to_real' x) = x"
  by (smt (verit, ccfv_SIG) assms bij_betw_iff_bijections bij_reals_norms to_real')

lemma to_real'_norm [simp]:
  shows "to_real' (of_real' (⟪a⟫)) = (⟪a⟫)"
  using norms_def to_real'
  by auto
  
lemma gyronorm_of_real':
  assumes "x ∈ norms"
  shows "⟪of_real' x⟫ = abs x"
  unfolding of_real'_def gyronorm_def comp_def
proof (subst to_carrier)
  show "of_real x ∈ carrier"
    using assms norms_carrier by auto
next
  show "norm ((of_real::real⇒'b) x) = ¦x¦"
    using  norm_of_real
    by auto
qed

lemma gyronorm_abs_to_real':
  assumes "x ∈ reals" 
  shows "abs (to_real' x) = ⟪x⟫"
  using assms
  by (metis bij_betwE bij_betw_to_real' gyronorm_of_real' of_real')

definition oplusR :: "real ⇒ real ⇒ real"  (infixl "⊕⇩R" 100) where 
  "a ⊕⇩R b = to_real' (of_real' a ⊕ of_real' b)"

definition oinvR :: "real ⇒ real" ("⊖⇩R") where
  "⊖⇩R a = to_real' (⊖ (of_real' a))"

end

locale gyrocarrier_norms_embed = gyrocarrier_norms_embed' + 
  fixes scale :: "real ⇒ 'a ⇒ 'a" (infixl "⊗" 105) 
  assumes oplus_reals: "⋀ a b. ⟦a ∈ reals; b ∈ reals⟧ ⟹ a ⊕ b ∈ reals"
  assumes oinv_reals: "⋀ a. a ∈ reals ⟹ ⊖ a ∈ reals"
  assumes otimes_reals: "⋀ a r. a ∈ reals ⟹ r ⊗ a ∈ reals"
begin

definition otimesR :: "real ⇒ real ⇒ real" (infixl "⊗⇩R" 100) where
  "r ⊗⇩R a = to_real' (r ⊗ (of_real' a))"

lemma oplusR_norms:
  shows "⋀ a b. ⟦a ∈ norms; b ∈ norms⟧ ⟹ a ⊕⇩R b ∈ norms"
  by (metis bij_betwE bij_betw_to_real' bij_reals_norms oplusR_def oplus_reals)

lemma oinvR_norms:
  shows "⋀ a. a ∈ norms ⟹ ⊖⇩R a ∈ norms"
  by (metis bij_betwE bij_betw_to_real' bij_reals_norms oinvR_def oinv_reals)

lemma otimesR_norms:
  shows "⋀ a r. a ∈ norms ⟹ r ⊗⇩R a ∈ norms"
  by (metis bij_betwE bij_betw_to_real' bij_reals_norms otimesR_def otimes_reals)

lemma of_real'_oplusR [simp]:
  shows "of_real' ((⟪a⟫) ⊕⇩R (⟪b⟫)) = (of_real' (⟪a⟫) ⊕ of_real' (⟪b⟫))"
  unfolding oplusR_def
  by (smt (verit, ccfv_threshold) Un_iff bij_betw_iff_bijections bij_reals_norms mem_Collect_eq norms_def of_real' oplus_reals)

lemma of_real'_otimesR [simp]:
  shows "of_real' (r ⊗⇩R (⟪a⟫)) = r ⊗ (of_real' (⟪a⟫))"
  unfolding otimesR_def
  by (metis (mono_tags, lifting) Un_iff bij_betwE bij_reals_norms norms_def mem_Collect_eq of_real' otimes_reals)

lemma of_real'_oinvR [simp]:
  shows "of_real' (⊖⇩R (⟪a⟫)) = ⊖ (of_real' (⟪a⟫))"
  unfolding oinvR_def
  by (metis (mono_tags, lifting) Un_iff bij_betwE bij_reals_norms mem_Collect_eq norms_def of_real' oinv_reals)

end

locale gyrovector_space_norms_embed = 
  gyrocarrier to_carrier +
  gyrocarrier_norms_embed to_carrier +
  pre_gyrovector_space to_carrier
  for to_carrier :: "'a::gyrocommutative_gyrogroup ⇒ 'b::{real_inner, real_normed_algebra_1}" +
  assumes homogeneity: 
    "⋀ (r :: real) (a :: 'a).
         ⟪r ⊗ a⟫ = ¦r¦ ⊗⇩R (⟪a⟫)"
  assumes gyrotriangle: 
    "⋀ (a :: 'a) (b :: 'a). 
         ⟪a ⊕ b⟫ ≤ (⟪a⟫) ⊕⇩R (⟪b⟫)"
begin

lemma gyrodistance_gyrotriangle:
  shows "d⇩⊕ a c ≤ d⇩⊕ a b  ⊕⇩R d⇩⊕ b c"
proof-
  have "⟪⊖a ⊕ c⟫ = ⟪(⊖a ⊕ b) ⊕ gyr (⊖a) b (⊖b ⊕ c)⟫"
    using gyro_polygonal_addition_lemma[of a b c]
    by auto
  also have "... ≤  (⟪⊖a ⊕ b⟫) ⊕⇩R (⟪gyr (⊖a) b (⊖b ⊕ c)⟫)"
    by (simp add: gyrotriangle)
  finally show ?thesis
    unfolding gyrodistance_def norm_gyr
    by meson
qed

end


end