Imports
Contraction of Real Lorentz vectors
@[ expose ] public section
The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a
covariant Lorentz vector.
def contrModCoModBi ( d : ℕ ) : ContrMod d →ₗ[ ℝ ] CoMod d →ₗ[ ℝ ] ℝ where
toFun ψ := {
toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ ,
map_add' := by d✝ : ℕ d : ℕ ψ : ContrMod d ⊢ ∀ ( x y : CoMod d ), ψ . toFin1dℝ ⬝ᵥ ( x + y ) . toFin1dℝ = ψ . toFin1dℝ ⬝ᵥ x . toFin1dℝ + ψ . toFin1dℝ ⬝ᵥ y . toFin1dℝ
intro φ φ' d✝ : ℕ d : ℕ ψ : ContrMod d φ : CoMod d φ' : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ ( φ + φ' ) . toFin1dℝ = ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ + ψ . toFin1dℝ ⬝ᵥ φ' . toFin1dℝ
simp only [ map_add ] d✝ : ℕ d : ℕ ψ : ContrMod d φ : CoMod d φ' : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ ( CoMod.toFin1dℝEquiv φ + CoMod.toFin1dℝEquiv φ' ) = ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ + ψ . toFin1dℝ ⬝ᵥ φ' . toFin1dℝ
rw [ dotProduct_add d✝ : ℕ d : ℕ ψ : ContrMod d φ : CoMod d φ' : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ CoMod.toFin1dℝEquiv φ + ψ . toFin1dℝ ⬝ᵥ CoMod.toFin1dℝEquiv φ' =
ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ + ψ . toFin1dℝ ⬝ᵥ φ' . toFin1dℝ All goals completed! 🐙 ] All goals completed! 🐙
map_smul' := by d✝ : ℕ d : ℕ ψ : ContrMod d ⊢ ∀ ( m : ℝ ) ( x : CoMod d ), ψ . toFin1dℝ ⬝ᵥ ( m • x ) . toFin1dℝ = ( RingHom.id ℝ ) m • ( ψ . toFin1dℝ ⬝ᵥ x . toFin1dℝ )
intro r φ d✝ : ℕ d : ℕ ψ : ContrMod d r : ℝ φ : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ ( r • φ ) . toFin1dℝ = ( RingHom.id ℝ ) r • ( ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ )
simp only [ LinearEquiv.map_smul ] d✝ : ℕ d : ℕ ψ : ContrMod d r : ℝ φ : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ r • CoMod.toFin1dℝEquiv φ = ( RingHom.id ℝ ) r • ( ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ )
rw [ dotProduct_smul d✝ : ℕ d : ℕ ψ : ContrMod d r : ℝ φ : CoMod d ⊢ r • ( ψ . toFin1dℝ ⬝ᵥ CoMod.toFin1dℝEquiv φ ) = ( RingHom.id ℝ ) r • ( ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ ) d✝ : ℕ d : ℕ ψ : ContrMod d r : ℝ φ : CoMod d ⊢ r • ( ψ . toFin1dℝ ⬝ᵥ CoMod.toFin1dℝEquiv φ ) = ( RingHom.id ℝ ) r • ( ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ ) ] d✝ : ℕ d : ℕ ψ : ContrMod d r : ℝ φ : CoMod d ⊢ r • ( ψ . toFin1dℝ ⬝ᵥ CoMod.toFin1dℝEquiv φ ) = ( RingHom.id ℝ ) r • ( ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ )
rfl All goals completed! 🐙 }
map_add' ψ ψ' := by d✝ : ℕ d : ℕ ψ : ContrMod d ψ' : ContrMod d ⊢ { toFun := fun φ => ( ψ + ψ' ) . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } =
{ toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } +
{ toFun := fun φ => ψ' . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ }
refine LinearMap.ext ( fun φ => ? _ ) d✝ : ℕ d : ℕ ψ : ContrMod d ψ' : ContrMod d φ : CoMod d ⊢ { toFun := fun φ => ( ψ + ψ' ) . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } φ =
( { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } +
{ toFun := fun φ => ψ' . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } )
φ
simp only [ map_add , LinearMap.coe_mk , AddHom.coe_mk , LinearMap.add_apply ] d✝ : ℕ d : ℕ ψ : ContrMod d ψ' : ContrMod d φ : CoMod d ⊢ ( ContrMod.toFin1dℝEquiv ψ + ContrMod.toFin1dℝEquiv ψ' ) ⬝ᵥ φ . toFin1dℝ =
ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ + ψ' . toFin1dℝ ⬝ᵥ φ . toFin1dℝ
rw [ add_dotProduct d✝ : ℕ d : ℕ ψ : ContrMod d ψ' : ContrMod d φ : CoMod d ⊢ ContrMod.toFin1dℝEquiv ψ ⬝ᵥ φ . toFin1dℝ + ContrMod.toFin1dℝEquiv ψ' ⬝ᵥ φ . toFin1dℝ =
ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ + ψ' . toFin1dℝ ⬝ᵥ φ . toFin1dℝ All goals completed! 🐙 ] All goals completed! 🐙
map_smul' r ψ := by d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d ⊢ { toFun := fun φ => ( r • ψ ) . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } =
( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ }
refine LinearMap.ext ( fun φ => ? _ ) d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d φ : CoMod d ⊢ { toFun := fun φ => ( r • ψ ) . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } φ =
( ( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) φ
simp only [ LinearEquiv.map_smul , LinearMap.coe_mk , AddHom.coe_mk ] d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d φ : CoMod d ⊢ r • ContrMod.toFin1dℝEquiv ψ ⬝ᵥ φ . toFin1dℝ =
( ( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) φ
rw [ smul_dotProduct d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d φ : CoMod d ⊢ r • ( ContrMod.toFin1dℝEquiv ψ ⬝ᵥ φ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) φ d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d φ : CoMod d ⊢ r • ( ContrMod.toFin1dℝEquiv ψ ⬝ᵥ φ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) φ ] d✝ : ℕ d : ℕ r : ℝ ψ : ContrMod d φ : CoMod d ⊢ r • ( ContrMod.toFin1dℝEquiv ψ ⬝ᵥ φ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun φ => ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) φ
rfl All goals completed! 🐙
The bi-linear map corresponding to contraction of a covariant Lorentz vector with a
contravariant Lorentz vector.
def coModContrModBi ( d : ℕ ) : CoMod d →ₗ[ ℝ ] ContrMod d →ₗ[ ℝ ] ℝ where
toFun φ := {
toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ ,
map_add' := by d✝ : ℕ d : ℕ φ : CoMod d ⊢ ∀ ( x y : ContrMod d ), φ . toFin1dℝ ⬝ᵥ ( x + y ) . toFin1dℝ = φ . toFin1dℝ ⬝ᵥ x . toFin1dℝ + φ . toFin1dℝ ⬝ᵥ y . toFin1dℝ
intro ψ ψ' d✝ : ℕ d : ℕ φ : CoMod d ψ : ContrMod d ψ' : ContrMod d ⊢ φ . toFin1dℝ ⬝ᵥ ( ψ + ψ' ) . toFin1dℝ = φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ + φ . toFin1dℝ ⬝ᵥ ψ' . toFin1dℝ
simp only [ map_add ] d✝ : ℕ d : ℕ φ : CoMod d ψ : ContrMod d ψ' : ContrMod d ⊢ φ . toFin1dℝ ⬝ᵥ ( ContrMod.toFin1dℝEquiv ψ + ContrMod.toFin1dℝEquiv ψ' ) =
φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ + φ . toFin1dℝ ⬝ᵥ ψ' . toFin1dℝ
rw [ dotProduct_add d✝ : ℕ d : ℕ φ : CoMod d ψ : ContrMod d ψ' : ContrMod d ⊢ φ . toFin1dℝ ⬝ᵥ ContrMod.toFin1dℝEquiv ψ + φ . toFin1dℝ ⬝ᵥ ContrMod.toFin1dℝEquiv ψ' =
φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ + φ . toFin1dℝ ⬝ᵥ ψ' . toFin1dℝ All goals completed! 🐙 ] All goals completed! 🐙
map_smul' := by d✝ : ℕ d : ℕ φ : CoMod d ⊢ ∀ ( m : ℝ ) ( x : ContrMod d ), φ . toFin1dℝ ⬝ᵥ ( m • x ) . toFin1dℝ = ( RingHom.id ℝ ) m • ( φ . toFin1dℝ ⬝ᵥ x . toFin1dℝ )
intro r ψ d✝ : ℕ d : ℕ φ : CoMod d r : ℝ ψ : ContrMod d ⊢ φ . toFin1dℝ ⬝ᵥ ( r • ψ ) . toFin1dℝ = ( RingHom.id ℝ ) r • ( φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ )
simp only [ LinearEquiv.map_smul ] d✝ : ℕ d : ℕ φ : CoMod d r : ℝ ψ : ContrMod d ⊢ φ . toFin1dℝ ⬝ᵥ r • ContrMod.toFin1dℝEquiv ψ = ( RingHom.id ℝ ) r • ( φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ )
rw [ dotProduct_smul d✝ : ℕ d : ℕ φ : CoMod d r : ℝ ψ : ContrMod d ⊢ r • ( φ . toFin1dℝ ⬝ᵥ ContrMod.toFin1dℝEquiv ψ ) = ( RingHom.id ℝ ) r • ( φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ ) d✝ : ℕ d : ℕ φ : CoMod d r : ℝ ψ : ContrMod d ⊢ r • ( φ . toFin1dℝ ⬝ᵥ ContrMod.toFin1dℝEquiv ψ ) = ( RingHom.id ℝ ) r • ( φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ ) ] d✝ : ℕ d : ℕ φ : CoMod d r : ℝ ψ : ContrMod d ⊢ r • ( φ . toFin1dℝ ⬝ᵥ ContrMod.toFin1dℝEquiv ψ ) = ( RingHom.id ℝ ) r • ( φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ )
rfl All goals completed! 🐙 }
map_add' φ φ' := by d✝ : ℕ d : ℕ φ : CoMod d φ' : CoMod d ⊢ { toFun := fun ψ => ( φ + φ' ) . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } =
{ toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } +
{ toFun := fun ψ => φ' . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ }
refine LinearMap.ext ( fun ψ => ? _ ) d✝ : ℕ d : ℕ φ : CoMod d φ' : CoMod d ψ : ContrMod d ⊢ { toFun := fun ψ => ( φ + φ' ) . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ψ =
( { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } +
{ toFun := fun ψ => φ' . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } )
ψ
simp only [ map_add , LinearMap.coe_mk , AddHom.coe_mk , LinearMap.add_apply ] d✝ : ℕ d : ℕ φ : CoMod d φ' : CoMod d ψ : ContrMod d ⊢ ( CoMod.toFin1dℝEquiv φ + CoMod.toFin1dℝEquiv φ' ) ⬝ᵥ ψ . toFin1dℝ = φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ + φ' . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ
rw [ add_dotProduct d✝ : ℕ d : ℕ φ : CoMod d φ' : CoMod d ψ : ContrMod d ⊢ CoMod.toFin1dℝEquiv φ ⬝ᵥ ψ . toFin1dℝ + CoMod.toFin1dℝEquiv φ' ⬝ᵥ ψ . toFin1dℝ =
φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ + φ' . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ All goals completed! 🐙 ] All goals completed! 🐙
map_smul' r φ := by d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ⊢ { toFun := fun ψ => ( r • φ ) . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } =
( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ }
refine LinearMap.ext ( fun ψ => ? _ ) d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ψ : ContrMod d ⊢ { toFun := fun ψ => ( r • φ ) . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ψ =
( ( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) ψ
simp only [ LinearEquiv.map_smul , LinearMap.coe_mk , AddHom.coe_mk ] d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ψ : ContrMod d ⊢ r • CoMod.toFin1dℝEquiv φ ⬝ᵥ ψ . toFin1dℝ =
( ( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) ψ
rw [ smul_dotProduct d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ψ : ContrMod d ⊢ r • ( CoMod.toFin1dℝEquiv φ ⬝ᵥ ψ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) ψ d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ψ : ContrMod d ⊢ r • ( CoMod.toFin1dℝEquiv φ ⬝ᵥ ψ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) ψ ] d✝ : ℕ d : ℕ r : ℝ φ : CoMod d ψ : ContrMod d ⊢ r • ( CoMod.toFin1dℝEquiv φ ⬝ᵥ ψ . toFin1dℝ ) =
( ( RingHom.id ℝ ) r • { toFun := fun ψ => φ . toFin1dℝ ⬝ᵥ ψ . toFin1dℝ , map_add' := ⋯ , map_smul' := ⋯ } ) ψ
rfl All goals completed! 🐙
The linear map from ContrMod d ⊗ CoMod d to ℝ given by
summing over components of contravariant Lorentz vector and
covariant Lorentz vector in the
standard basis (i.e. the dot product).
In terms of index notation this is the contraction is ψⁱ φᵢ.
def contrCoContract : ( ( ContrMod.rep ) . tprod ( CoMod.rep ) ) . IntertwiningMap
( Representation.trivial ℝ ( LorentzGroup d ) ℝ ) where
toLinearMap := TensorProduct.lift ( contrModCoModBi d )
isIntertwining' Λ := by d : ℕ Λ : ↑ ( LorentzGroup d ) ⊢ TensorProduct.lift ( contrModCoModBi d ) ∘ₗ ( ContrMod.rep . tprod CoMod.rep ) Λ =
( Representation.trivial ℝ ↑ ( LorentzGroup d ) ℝ ) Λ ∘ₗ TensorProduct.lift ( contrModCoModBi d )
ext ψ φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( ( AlgebraTensorModule.curry ( TensorProduct.lift ( contrModCoModBi d ) ∘ₗ ( ContrMod.rep . tprod CoMod.rep ) Λ ) ) ψ ) φ =
( ( AlgebraTensorModule.curry
( ( Representation.trivial ℝ ↑ ( LorentzGroup d ) ℝ ) Λ ∘ₗ TensorProduct.lift ( contrModCoModBi d ) ) )
ψ )
φ
simp only [ Representation.tprod_apply , AlgebraTensorModule.curry_apply ,
LinearMap.restrictScalars_self , curry_apply , LinearMap.coe_comp , Function.comp_apply ,
map_tmul , lift.tmul , Representation.isTrivial_def , LinearMap.id_comp ] d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( ( contrModCoModBi d ) ( ( ContrMod.rep Λ ) ψ ) ) ( ( CoMod.rep Λ ) φ ) = ( ( contrModCoModBi d ) ψ ) φ
change ( Λ . 1 *ᵥ ψ . toFin1dℝ ) ⬝ᵥ ( ( LorentzGroup.transpose Λ ⁻¹ ) . 1 *ᵥ φ . toFin1dℝ ) = _ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ↑ Λ *ᵥ ψ . toFin1dℝ ⬝ᵥ ↑ ( LorentzGroup.transpose Λ ⁻¹ ) *ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ
rw [ dotProduct_mulVec , d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( ↑ Λ *ᵥ ψ . toFin1dℝ ) ᵥ* ↑ ( LorentzGroup.transpose Λ ⁻¹ ) ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ LorentzGroup.transpose_val , d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( ↑ Λ *ᵥ ψ . toFin1dℝ ) ᵥ* (↑ Λ ⁻¹ ) ᵀ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ
vecMul_transpose , d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ↑ Λ ⁻¹ *ᵥ ↑ Λ *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ mulVec_mulVec , d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( ↑ Λ ⁻¹ * ↑ Λ ) *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ LorentzGroup.coe_inv , d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ( (↑ Λ ) ⁻¹ * ↑ Λ ) *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ inv_mul_of_invertible Λ . 1 d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ ] d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ 1 *ᵥ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ
simp only [ one_mulVec ] d : ℕ Λ : ↑ ( LorentzGroup d ) ψ : ContrMod d φ : CoMod d ⊢ ψ . toFin1dℝ ⬝ᵥ φ . toFin1dℝ = ( ( contrModCoModBi d ) ψ ) φ
rfl All goals completed! 🐙
Notation for contrCoContract acting on a tmul.
The linear map from CoMod d ⊗ ContrMod d to ℝ given by
summing over components of contravariant Lorentz vector and
covariant Lorentz vector in the
standard basis (i.e. the dot product).
In terms of index notation this is the contraction is ψⁱ φᵢ.
Notation for coContrContract acting on a tmul.
Symmetry relations
Contracting contr vectors with contr vectors etc.
The linear map from ContrMod d ⊗ ContrMod d to ℝ induced by the homomorphism
Contr.toCo and the contraction contrCoContract.
The linear map from ContrMod d ⊗ ContrMod d to ℝ induced by the homomorphism
Contr.toCo and the contraction contrCoContract.
Notation for contrContrContractField acting on a tmul.
The linear map from CoMod d ⊗ CoMod d to ℝ induced by the homomorphism
Co.toContr and the contraction coContrContract.
Notation for coCoContract acting on a tmul.
We derive the lemmas in main for contrContrContractField.
@[ simp ]
lemma action_tmul ( g : LorentzGroup d ) : ⟪ ContrMod.rep g x , ContrMod.rep g y ⟫ₘ = ⟪ x , y ⟫ₘ :=
LinearMap.congr_fun ( contrContrContract . isIntertwining' g ) ( x ⊗ₜ[ ℝ ] y )
lemma as_sum : ⟪ x , y ⟫ₘ = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) := by d : ℕ x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] y ) = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i )
rw [ contrContrContract_hom_tmul d : ℕ x : ContrMod d y : ContrMod d ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) d : ℕ x : ContrMod d y : ContrMod d ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i )
simp only [ dotProduct , minkowskiMatrix , LieAlgebra.Orthogonal.indefiniteDiagonal , mulVec_diagonal ,
Fintype.sum_sum_type , Finset.univ_unique , Fin.default_eq_zero , Fin.isValue , Sum.elim_inl ,
one_mul , Finset.sum_singleton , Sum.elim_inr , neg_mul , mul_neg , Finset.sum_neg_distrib ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . toFin1dℝ ( Sum.inl 0 ) * y . toFin1dℝ ( Sum.inl 0 ) + - ∑ x_1 , x . toFin1dℝ ( Sum.inr x_1 ) * y . toFin1dℝ ( Sum.inr x_1 ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i )
rfl All goals completed! 🐙
lemma as_sum_toSpace : ⟪ x , y ⟫ₘ = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) -
⟪ x . toSpace , y . toSpace ⟫_ ℝ := by d : ℕ x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] y ) = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ⟪ x . toSpace , y . toSpace ⟫_ ℝ
rw [ as_sum d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ⟪ x . toSpace , y . toSpace ⟫_ ℝ d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ⟪ x . toSpace , y . toSpace ⟫_ ℝ ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ⟪ x . toSpace , y . toSpace ⟫_ ℝ
congr e_a.e_f d : ℕ x : ContrMod d y : ContrMod d ⊢ (fun i => x . val ( Sum.inr i ) * y . val ( Sum.inr i ) ) = fun i => ⟪ x . toSpace . ofLp i , y . toSpace . ofLp i ⟫_ ℝ
funext i e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = ⟪ x . toSpace . ofLp i , y . toSpace . ofLp i ⟫_ ℝ
rw [ mul_comm e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ y . val ( Sum.inr i ) * x . val ( Sum.inr i ) = ⟪ x . toSpace . ofLp i , y . toSpace . ofLp i ⟫_ ℝ e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ y . val ( Sum.inr i ) * x . val ( Sum.inr i ) = ⟪ x . toSpace . ofLp i , y . toSpace . ofLp i ⟫_ ℝ ] e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ y . val ( Sum.inr i ) * x . val ( Sum.inr i ) = ⟪ x . toSpace . ofLp i , y . toSpace . ofLp i ⟫_ ℝ
rfl All goals completed! 🐙
lemma stdBasis_inl { d : ℕ } :
⟪ @ ContrMod.stdBasis d ( Sum.inl 0 ) , ContrMod.stdBasis ( Sum.inl 0 ) ⟫ₘ = ( 1 : ℝ ) := by d : ℕ ⊢ contrContrContractField ( ContrMod.stdBasis ( Sum.inl 0 ) ⊗ₜ[ ℝ ] ContrMod.stdBasis ( Sum.inl 0 ) ) = 1
rw [ as_sum d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) =
1 d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) =
1 ] d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) =
1
trans ( 1 : ℝ ) - ( 0 : ℝ ) d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) =
1 - 0 d : ℕ ⊢ 1 - 0 = 1
congr e_a d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) = 1 e_a d : ℕ ⊢ ∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) = 0 d : ℕ ⊢ 1 - 0 = 1
· e_a d : ℕ ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inl 0 ) = 1 rw [ ContrMod.stdBasis_apply_same e_a d : ℕ ⊢ 1 * 1 = 1 e_a d : ℕ ⊢ 1 * 1 = 1 ] e_a d : ℕ ⊢ 1 * 1 = 1
simp All goals completed! 🐙
· e_a d : ℕ ⊢ ∑ i , ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr i ) = 0 rw [ Fintype.sum_eq_zero e_a d : ℕ ⊢ 0 = 0 e_a.h d : ℕ ⊢ ∀ ( a : Fin d ), ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) = 0 e_a.h d : ℕ ⊢ ∀ ( a : Fin d ), ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) = 0 ] e_a.h d : ℕ ⊢ ∀ ( a : Fin d ), ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) = 0
intro a e_a.h d : ℕ a : Fin d ⊢ ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) * ( ContrMod.stdBasis ( Sum.inl 0 ) ) . val ( Sum.inr a ) = 0
simp All goals completed! 🐙
· d : ℕ ⊢ 1 - 0 = 1 ring All goals completed! 🐙
lemma symm : ⟪ x , y ⟫ₘ = ⟪ y , x ⟫ₘ := by d : ℕ x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] y ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ as_sum , d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i ) as_sum d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i ) d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i ) ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) - ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) =
y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i )
congr 1 e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) = y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i )
rw [ mul_comm e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) = y . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i ) e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i ) ] e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = ∑ i , y . val ( Sum.inr i ) * x . val ( Sum.inr i )
congr e_a.e_f d : ℕ x : ContrMod d y : ContrMod d ⊢ (fun i => x . val ( Sum.inr i ) * y . val ( Sum.inr i ) ) = fun i => y . val ( Sum.inr i ) * x . val ( Sum.inr i )
funext i e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ x . val ( Sum.inr i ) * y . val ( Sum.inr i ) = y . val ( Sum.inr i ) * x . val ( Sum.inr i )
rw [ mul_comm e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ y . val ( Sum.inr i ) * x . val ( Sum.inr i ) = y . val ( Sum.inr i ) * x . val ( Sum.inr i ) All goals completed! 🐙 ] All goals completed! 🐙
lemma dual_mulVec_right : ⟪ x , dual Λ *ᵥ y ⟫ₘ = ⟪ Λ *ᵥ x , y ⟫ₘ := by d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( dual Λ *ᵥ y ) ) = contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] y )
rw [ contrContrContract_hom_tmul , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ ( dual Λ *ᵥ y ) . toFin1dℝ = contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] y ) d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ ( dual Λ *ᵥ y ) . toFin1dℝ = ( Λ *ᵥ x ) . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ contrContrContract_hom_tmul d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ ( dual Λ *ᵥ y ) . toFin1dℝ = ( Λ *ᵥ x ) . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ ( dual Λ *ᵥ y ) . toFin1dℝ = ( Λ *ᵥ x ) . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ ] d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ η *ᵥ ( dual Λ *ᵥ y ) . toFin1dℝ = ( Λ *ᵥ x ) . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ
simp only [ ContrMod.mulVec_toFin1dℝ , mulVec_mulVec ] d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ ( η * dual Λ ) *ᵥ y . toFin1dℝ = Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ
simp only [ dual , ← mul_assoc , minkowskiMatrix.sq , one_mul ] d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ ( Λ ᵀ * η ) *ᵥ y . toFin1dℝ = Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ
rw [ ← mulVec_mulVec , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ⬝ᵥ Λ ᵀ *ᵥ η *ᵥ y . toFin1dℝ = Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ All goals completed! 🐙 dotProduct_mulVec , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ x . toFin1dℝ ᵥ* Λ ᵀ ⬝ᵥ η *ᵥ y . toFin1dℝ = Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ All goals completed! 🐙 vecMul_transpose d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ = Λ *ᵥ x . toFin1dℝ ⬝ᵥ η *ᵥ y . toFin1dℝ All goals completed! 🐙 ] All goals completed! 🐙
lemma dual_mulVec_left : ⟪ dual Λ *ᵥ x , y ⟫ₘ = ⟪ x , Λ *ᵥ y ⟫ₘ := by d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( ( dual Λ *ᵥ x ) ⊗ₜ[ ℝ ] y ) = contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) )
rw [ symm , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( dual Λ *ᵥ x ) ) = contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) All goals completed! 🐙 dual_mulVec_right , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] x ) = contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) All goals completed! 🐙 symm d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) = contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) All goals completed! 🐙 ] All goals completed! 🐙
lemma right_parity : ⟪ x , ContrMod.rep LorentzGroup.parity y ⟫ₘ = ∑ i , x . val i * y . val i := by d : ℕ x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = ∑ i , x . val i * y . val i
rw [ as_sum d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
∑ i , x . val i * y . val i d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
∑ i , x . val i * y . val i ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
∑ i , x . val i * y . val i
simp only [ Fin.isValue , Fintype.sum_sum_type , Finset.univ_unique , Fin.default_eq_zero ,
Finset.sum_singleton ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) + ∑ a₂ , x . val ( Sum.inr a₂ ) * y . val ( Sum.inr a₂ )
trans x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) +
∑ i : Fin d , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) +
∑ i , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) +
∑ i , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) =
x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) + ∑ a₂ , x . val ( Sum.inr a₂ ) * y . val ( Sum.inr a₂ )
· d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) +
∑ i , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) simp only [ Fin.isValue , Finset.sum_neg_distrib ] d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) -
∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) =
x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) +
- ∑ i , x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i )
rfl All goals completed! 🐙
congr 1 e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) =
∑ a₂ , x . val ( Sum.inr a₂ ) * y . val ( Sum.inr a₂ )
· e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inl 0 ) = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 ) change x . val ( Sum.inl 0 ) * ( η *ᵥ y . toFin1dℝ ) ( Sum.inl 0 ) = _ e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ x . val ( Sum.inl 0 ) * ( η *ᵥ y . toFin1dℝ ) ( Sum.inl 0 ) = x . val ( Sum.inl 0 ) * y . val ( Sum.inl 0 )
simp only [ Fin.isValue , mulVec_inl_0 , mul_eq_mul_left_iff ] e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ y . toFin1dℝ ( Sum.inl 0 ) = y . val ( Sum.inl 0 ) ∨ x . val ( Sum.inl 0 ) = 0
exact mul_eq_mul_left_iff . mp rfl All goals completed! 🐙
· e_a d : ℕ x : ContrMod d y : ContrMod d ⊢ ∑ i , - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) =
∑ a₂ , x . val ( Sum.inr a₂ ) * y . val ( Sum.inr a₂ ) congr e_a.e_f d : ℕ x : ContrMod d y : ContrMod d ⊢ (fun i => - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) ) = fun a₂ =>
x . val ( Sum.inr a₂ ) * y . val ( Sum.inr a₂ )
funext i e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ - ( x . val ( Sum.inr i ) * ( ( ContrMod.rep LorentzGroup.parity ) y ) . val ( Sum.inr i ) ) = x . val ( Sum.inr i ) * y . val ( Sum.inr i )
change - ( x . val ( Sum.inr i ) * ( ( η *ᵥ y . toFin1dℝ ) ( Sum.inr i ) ) ) = _ e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ - ( x . val ( Sum.inr i ) * ( η *ᵥ y . toFin1dℝ ) ( Sum.inr i ) ) = x . val ( Sum.inr i ) * y . val ( Sum.inr i )
simp only [ mulVec_inr_i , mul_neg , neg_neg , mul_eq_mul_left_iff ] e_a.e_f d : ℕ x : ContrMod d y : ContrMod d i : Fin d ⊢ y . toFin1dℝ ( Sum.inr i ) = y . val ( Sum.inr i ) ∨ x . val ( Sum.inr i ) = 0
exact mul_eq_mul_left_iff . mp rfl All goals completed! 🐙
lemma self_parity_eq_zero_iff : ⟪ y , ContrMod.rep LorentzGroup.parity y ⟫ₘ = 0 ↔ y = 0 := by d : ℕ y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = 0 ↔ y = 0
refine Iff.intro ( fun h => ? _ ) ( fun h => ? _ ) refine_1 d : ℕ y : ContrMod d h : contrContrContractField ( y ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = 0 ⊢ y = 0 refine_2 d : ℕ y : ContrMod d h : y = 0 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = 0
· refine_1 d : ℕ y : ContrMod d h : contrContrContractField ( y ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = 0 ⊢ y = 0 rw [ right_parity refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 ⊢ y = 0 refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 ⊢ y = 0 ] at h refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 ⊢ y = 0
have hn := Fintype.sum_eq_zero_iff_of_nonneg ( f := fun i => y . val i * y . val i ) ( fun i => by d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 i : Fin 1 ⊕ Fin d ⊢ 0 i ≤ (fun i => y . val i * y . val i ) i refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : ∑ i , y . val i * y . val i = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0
simpa using mul_self_nonneg ( y . val i ) All goals completed! 🐙 refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : ∑ i , y . val i * y . val i = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0 ) refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : ∑ i , y . val i * y . val i = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0
rw [ h refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : 0 = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0 refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : 0 = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0 ] at hn refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : 0 = 0 ↔ (fun i => y . val i * y . val i ) = 0 ⊢ y = 0
simp only [ true_iff ] at hn refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 ⊢ y = 0
apply ContrMod.ext refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 ⊢ y . val = ContrMod.val 0
funext i refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 i : Fin 1 ⊕ Fin d ⊢ y . val i = ContrMod.val 0 i
have h1 := congrFun hn i refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 i : Fin 1 ⊕ Fin d h1 : y . val i * y . val i = 0 i ⊢ y . val i = ContrMod.val 0 i
simp only [ Pi.zero_apply , mul_eq_zero , or_self ] at h1 refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 i : Fin 1 ⊕ Fin d h1 : y . val i = 0 ⊢ y . val i = ContrMod.val 0 i
simp only [ h1 ] refine_1 d : ℕ y : ContrMod d h : ∑ i , y . val i * y . val i = 0 hn : (fun i => y . val i * y . val i ) = 0 i : Fin 1 ⊕ Fin d h1 : y . val i = 0 ⊢ 0 = ContrMod.val 0 i
rfl All goals completed! 🐙
· refine_2 d : ℕ y : ContrMod d h : y = 0 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) y ) = 0 rw [ h refine_2 d : ℕ y : ContrMod d h : y = 0 ⊢ contrContrContractField ( 0 ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) 0 ) = 0 refine_2 d : ℕ y : ContrMod d h : y = 0 ⊢ contrContrContractField ( 0 ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) 0 ) = 0 ] refine_2 d : ℕ y : ContrMod d h : y = 0 ⊢ contrContrContractField ( 0 ⊗ₜ[ ℝ ] ( ContrMod.rep LorentzGroup.parity ) 0 ) = 0
simp only [ map_zero , tmul_zero ] All goals completed! 🐙
The metric tensor is non-degenerate.
set_option backward.isDefEq.respectTransparency false in
lemma matrix_apply_eq_iff_sub : ⟪ x , Λ *ᵥ y ⟫ₘ = ⟪ x , Λ' *ᵥ y ⟫ₘ ↔ ⟪ x , ( Λ - Λ' ) *ᵥ y ⟫ₘ = 0 := by d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) = contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ' *ᵥ y ) ) ↔
contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0
rw [ ← sub_eq_zero , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ' *ᵥ y ) ) = 0 ↔
contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0 All goals completed! 🐙 ← LinearMap.map_sub , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - x ⊗ₜ[ ℝ ] ( Λ' *ᵥ y ) ) = 0 ↔
contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0 All goals completed! 🐙 ← tmul_sub , d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( Λ *ᵥ y - Λ' *ᵥ y ) ) = 0 ↔ contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0 All goals completed! 🐙 ← ContrMod.sub_mulVec Λ Λ' y d : ℕ x : ContrMod d y : ContrMod d Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0 ↔ contrContrContractField ( x ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ y ) ) = 0 All goals completed! 🐙 ] All goals completed! 🐙
lemma matrix_eq_iff_eq_forall' : ( ∀ ( v : ContrMod d ) , ( Λ *ᵥ v ) = Λ' *ᵥ v ) ↔
∀ ( w v : ContrMod d ) , ⟪ v , Λ *ᵥ w ⟫ₘ = ⟪ v , Λ' *ᵥ w ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ) ↔
∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) )
refine Iff.intro ( fun h ↦ fun w v ↦ ? _ ) ( fun h ↦ fun v ↦ ? _ ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v w : ContrMod d v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) v : ContrMod d ⊢ Λ *ᵥ v = Λ' *ᵥ v
· refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v w : ContrMod d v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) rw [ h w refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v w : ContrMod d v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) All goals completed! 🐙 ] All goals completed! 🐙
· refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) ) v : ContrMod d ⊢ Λ *ᵥ v = Λ' *ᵥ v simp only [ matrix_apply_eq_iff_sub ] at h refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 ⊢ Λ *ᵥ v = Λ' *ᵥ v
refine sub_eq_zero . 1 ? _ refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0
have h1 := h v refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 h1 : ∀ ( v_1 : ContrMod d ), contrContrContractField ( v_1 ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ v ) ) = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0
rw [ nondegenerate refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 h1 : ( Λ - Λ' ) *ᵥ v = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0 refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 h1 : ( Λ - Λ' ) *ᵥ v = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0 ] at h1 refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 h1 : ( Λ - Λ' ) *ᵥ v = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0
simp only [ ContrMod.sub_mulVec ] at h1 refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ v : ContrMod d h : ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( ( Λ - Λ' ) *ᵥ w ) ) = 0 h1 : Λ *ᵥ v - Λ' *ᵥ v = 0 ⊢ Λ *ᵥ v - Λ' *ᵥ v = 0
exact h1 All goals completed! 🐙
lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ ( w v : ContrMod d ) , ⟪ v , Λ *ᵥ w ⟫ₘ = ⟪ v , Λ' *ᵥ w ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ = Λ' ↔ ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ' *ᵥ w ) )
rw [ ← matrix_eq_iff_eq_forall' d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ = Λ' ↔ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ = Λ' ↔ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ = Λ' ↔ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v
refine Iff.intro ( fun h => ? _ ) ( fun h => ? _ ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ = Λ' ⊢ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ⊢ Λ = Λ'
· refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ = Λ' ⊢ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v subst h refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ *ᵥ v
exact fun v => rfl All goals completed! 🐙
· refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ⊢ Λ = Λ' rw [ ← ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm . apply_eq_iff_eq refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ⊢ ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ =
( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ' refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ⊢ ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ =
( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ' ] refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v ⊢ ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ =
( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ'
ext1 v refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ Λ' : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( v : ContrMod d ), Λ *ᵥ v = Λ' *ᵥ v v : ContrMod d ⊢ ( ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ ) v =
( ( LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis ) . toEquiv . symm Λ' ) v
exact h v All goals completed! 🐙
lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ ( w v : ContrMod d ) , ⟪ v , Λ *ᵥ w ⟫ₘ = ⟪ v , w ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ = 1 ↔ ∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w )
rw [ matrix_eq_iff_eq_forall d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( 1 *ᵥ w ) ) ) ↔
∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( 1 *ᵥ w ) ) ) ↔
∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] ( 1 *ᵥ w ) ) ) ↔
∀ ( w v : ContrMod d ), contrContrContractField ( v ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w )
simp only [ ContrMod.one_mulVec ] All goals completed! 🐙
lemma _root_.LorentzGroup.mem_iff_invariant : Λ ∈ LorentzGroup d ↔
∀ ( w v : ContrMod d ) , ⟪ Λ *ᵥ v , Λ *ᵥ w ⟫ₘ = ⟪ v , w ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ ∈ LorentzGroup d ↔
∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w )
refine Iff.intro ( fun h => ? _ ) ( fun h => ? _ ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d ⊢ ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ⊢ Λ ∈ LorentzGroup d
· refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d ⊢ ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) intro x y refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ← dual_mulVec_right , refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( dual Λ *ᵥ Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ContrMod.mulVec_mulVec refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ] refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
have h1 := LorentzGroup.mem_iff_dual_mul_self . mp h refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d h1 : dual Λ * Λ = 1 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ h1 refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d h1 : dual Λ * Λ = 1 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( 1 *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d h1 : dual Λ * Λ = 1 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( 1 *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ] refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d h1 : dual Λ * Λ = 1 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] ( 1 *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ContrMod.one_mulVec refine_1 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : Λ ∈ LorentzGroup d x : ContrMod d y : ContrMod d h1 : dual Λ * Λ = 1 ⊢ contrContrContractField ( y ⊗ₜ[ ℝ ] x ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) All goals completed! 🐙 ] All goals completed! 🐙
· refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ⊢ Λ ∈ LorentzGroup d conv at h => d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) | ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w )
intro x y d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d | contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ← dual_mulVec_right , ContrMod.mulVec_mulVec ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d | contrContrContractField ( y ⊗ₜ[ ℝ ] ( ( dual Λ * Λ ) *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ← matrix_eq_id_iff refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : dual Λ * Λ = 1 ⊢ Λ ∈ LorentzGroup d refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : dual Λ * Λ = 1 ⊢ Λ ∈ LorentzGroup d ] at h refine_2 d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : dual Λ * Λ = 1 ⊢ Λ ∈ LorentzGroup d
exact LorentzGroup.mem_iff_dual_mul_self . mpr h All goals completed! 🐙
set_option backward.isDefEq.respectTransparency false in
lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
∀ ( w : ContrMod d ) , ⟪ Λ *ᵥ w , Λ *ᵥ w ⟫ₘ = ⟪ w , w ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ Λ ∈ LorentzGroup d ↔
∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w )
rw [ LorentzGroup.mem_iff_invariant d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ) ↔
∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ) ↔
∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ⊢ (∀ ( w v : ContrMod d ), contrContrContractField ( ( Λ *ᵥ v ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( v ⊗ₜ[ ℝ ] w ) ) ↔
∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w )
refine Iff.intro ( fun h x => h x x ) ( fun h x y => ? _ ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
have hp := h ( x + y ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ ( x + y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x + y ) ) ) = contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
have hn := h ( x - y ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ ( x + y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x + y ) ) ) = contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ContrMod.mulVec_add , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x + Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x + Λ *ᵥ y ) ) = contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) tmul_add , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x + Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ x + Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) =
contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) add_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ x + Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) =
contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) add_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] ( x + y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) tmul_add , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( ( x + y ) ⊗ₜ[ ℝ ] x + ( x + y ) ⊗ₜ[ ℝ ] y ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) add_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x + y ) ⊗ₜ[ ℝ ] y ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) add_tmul d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ] at hp d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ ( x - y ) ) ⊗ₜ[ ℝ ] ( Λ *ᵥ ( x - y ) ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ ContrMod.mulVec_sub , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x - Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x - Λ *ᵥ y ) ) = contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) tmul_sub , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x - Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ x - Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) =
contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) sub_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ x - Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) =
contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) sub_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] ( x - y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) tmul_sub , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( ( x - y ) ⊗ₜ[ ℝ ] x - ( x - y ) ⊗ₜ[ ℝ ] y ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) sub_tmul , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x - y ) ⊗ₜ[ ℝ ] y ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) sub_tmul d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ] at hn d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) + ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) + ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x + y ⊗ₜ[ ℝ ] x + ( x ⊗ₜ[ ℝ ] y + y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField
( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) - ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) - ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x - y ⊗ₜ[ ℝ ] x - ( x ⊗ₜ[ ℝ ] y - y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
simp only [ map_add , map_sub ] at hp hn d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( y ⊗ₜ[ ℝ ] x ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( y ⊗ₜ[ ℝ ] x ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
rw [ symm ( Λ *ᵥ y ) ( Λ *ᵥ x ) , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( y ⊗ₜ[ ℝ ] x ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( y ⊗ₜ[ ℝ ] x ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) symm y x d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ] at hp hn d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
let e : 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ≃ₗ[ ℝ ] ℝ :=
LinearEquiv.refl ℝ ( ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ⊢ contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) = contrContrContractField ( y ⊗ₜ[ ℝ ] x )
apply e . injective d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) = e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) )
have hp' := e . injective . eq_iff . mpr hp d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e
( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) = e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) )
have hn' := e . injective . eq_iff . mpr hn d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e
( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e
( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) = e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) )
simp only [ map_add , map_sub ] at hp' hn' d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) = e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) )
linear_combination ( norm := ring_nf a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0 ) ( 1 / 4 ) * hp' + ( - 1 / 4 ) * hn'
rw [ symm ( Λ *ᵥ y ) ( Λ *ᵥ x ) , a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( y ⊗ₜ[ ℝ ] x ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0 a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0 symm y x a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0 a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0 ] a d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ h : ∀ ( w : ContrMod d ), contrContrContractField ( ( Λ *ᵥ w ) ⊗ₜ[ ℝ ] ( Λ *ᵥ w ) ) = contrContrContractField ( w ⊗ₜ[ ℝ ] w ) x : ContrMod d y : ContrMod d hp : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) + contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) +
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) + contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) + contrContrContractField ( x ⊗ₜ[ ℝ ] y ) +
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) + contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) hn : contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) - contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) -
( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) - contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
contrContrContractField ( x ⊗ₜ[ ℝ ] x ) - contrContrContractField ( x ⊗ₜ[ ℝ ] y ) -
( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) - contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) e : ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) ≃ₗ[ ℝ ] ℝ := LinearEquiv.refl ℝ ↑ ( 𝟙_ ( Rep ℝ ↑ ( LorentzGroup d ) ) ) hp' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) +
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) +
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) + e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) hn' : e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ x ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) -
( e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) - e ( contrContrContractField ( ( Λ *ᵥ y ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) ) =
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) - e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
( e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) - e ( contrContrContractField ( y ⊗ₜ[ ℝ ] y ) ) ) ⊢ e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) + e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( x ⊗ₜ[ ℝ ] y ) ) -
e ( contrContrContractField ( ( Λ *ᵥ x ) ⊗ₜ[ ℝ ] ( Λ *ᵥ y ) ) ) =
0
simp All goals completed! 🐙
Some equalities and inequalities
lemma inl_sq_eq ( v : ContrMod d ) : v . val ( Sum.inl 0 ) ^ 2 =
( ⟪ v , v ⟫ₘ ) + ∑ i , v . val ( Sum.inr i ) ^ 2 := by d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 = contrContrContractField ( v ⊗ₜ[ ℝ ] v ) + ∑ i , v . val ( Sum.inr i ) ^ 2
rw [ as_sum d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 =
v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) - ∑ i , v . val ( Sum.inr i ) * v . val ( Sum.inr i ) + ∑ i , v . val ( Sum.inr i ) ^ 2 d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 =
v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) - ∑ i , v . val ( Sum.inr i ) * v . val ( Sum.inr i ) + ∑ i , v . val ( Sum.inr i ) ^ 2 ] d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 =
v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) - ∑ i , v . val ( Sum.inr i ) * v . val ( Sum.inr i ) + ∑ i , v . val ( Sum.inr i ) ^ 2
apply sub_eq_iff_eq_add . mp d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 - ∑ i , v . val ( Sum.inr i ) ^ 2 =
v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) - ∑ i , v . val ( Sum.inr i ) * v . val ( Sum.inr i )
congr e_a d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 = v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) e_a.e_f d : ℕ v : ContrMod d ⊢ (fun i => v . val ( Sum.inr i ) ^ 2 ) = fun i => v . val ( Sum.inr i ) * v . val ( Sum.inr i )
· e_a d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) ^ 2 = v . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) exact pow_two ( v . val ( Sum.inl 0 ) ) All goals completed! 🐙
· e_a.e_f d : ℕ v : ContrMod d ⊢ (fun i => v . val ( Sum.inr i ) ^ 2 ) = fun i => v . val ( Sum.inr i ) * v . val ( Sum.inr i ) funext i e_a.e_f d : ℕ v : ContrMod d i : Fin d ⊢ v . val ( Sum.inr i ) ^ 2 = v . val ( Sum.inr i ) * v . val ( Sum.inr i )
exact pow_two ( v . val ( Sum.inr i ) ) All goals completed! 🐙
lemma le_inl_sq ( v : ContrMod d ) : ⟪ v , v ⟫ₘ ≤ v . val ( Sum.inl 0 ) ^ 2 := by d : ℕ v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) ≤ v . val ( Sum.inl 0 ) ^ 2
rw [ inl_sq_eq d : ℕ v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) ≤ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) + ∑ i , v . val ( Sum.inr i ) ^ 2 d : ℕ v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) ≤ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) + ∑ i , v . val ( Sum.inr i ) ^ 2 ] d : ℕ v : ContrMod d ⊢ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) ≤ contrContrContractField ( v ⊗ₜ[ ℝ ] v ) + ∑ i , v . val ( Sum.inr i ) ^ 2
apply ( le_add_iff_nonneg_right _ ) . mpr d : ℕ v : ContrMod d ⊢ 0 ≤ ∑ i , v . val ( Sum.inr i ) ^ 2
refine Fintype.sum_nonneg ? hf hf d : ℕ v : ContrMod d ⊢ 0 ≤ fun i => v . val ( Sum.inr i ) ^ 2
exact fun i => pow_two_nonneg ( v . val ( Sum.inr i ) ) All goals completed! 🐙
lemma ge_abs_inner_product ( v w : ContrMod d ) : v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) -
‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤ ⟪ v , w ⟫ₘ := by d : ℕ v : ContrMod d w : ContrMod d ⊢ v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤ contrContrContractField ( v ⊗ₜ[ ℝ ] w )
rw [ as_sum_toSpace , d : ℕ v : ContrMod d w : ContrMod d ⊢ v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤
v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ⟪ v . toSpace , w . toSpace ⟫_ ℝ d : ℕ v : ContrMod d w : ContrMod d ⊢ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ≤ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ sub_le_sub_iff_left d : ℕ v : ContrMod d w : ContrMod d ⊢ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ≤ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ d : ℕ v : ContrMod d w : ContrMod d ⊢ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ≤ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ] d : ℕ v : ContrMod d w : ContrMod d ⊢ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ≤ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖
exact Real.le_norm_self ⟪ v . toSpace , w . toSpace ⟫_ ℝ All goals completed! 🐙
lemma ge_sub_norm ( v w : ContrMod d ) : v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) -
‖ v . toSpace ‖ * ‖ w . toSpace ‖ ≤ ⟪ v , w ⟫ₘ := by d : ℕ v : ContrMod d w : ContrMod d ⊢ v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ‖ v . toSpace ‖ * ‖ w . toSpace ‖ ≤ contrContrContractField ( v ⊗ₜ[ ℝ ] w )
apply le_trans _ ( ge_abs_inner_product v w ) d : ℕ v : ContrMod d w : ContrMod d ⊢ v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ‖ v . toSpace ‖ * ‖ w . toSpace ‖ ≤
v . val ( Sum.inl 0 ) * w . val ( Sum.inl 0 ) - ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖
rw [ sub_le_sub_iff_left d : ℕ v : ContrMod d w : ContrMod d ⊢ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤ ‖ v . toSpace ‖ * ‖ w . toSpace ‖ d : ℕ v : ContrMod d w : ContrMod d ⊢ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤ ‖ v . toSpace ‖ * ‖ w . toSpace ‖ ] d : ℕ v : ContrMod d w : ContrMod d ⊢ ‖ ⟪ v . toSpace , w . toSpace ⟫_ ℝ ‖ ≤ ‖ v . toSpace ‖ * ‖ w . toSpace ‖
exact norm_inner_le_norm v . toSpace w . toSpace All goals completed! 🐙
The Minkowski metric and the standard basis
@[ simp ]
lemma basis_left { v : ContrMod d } ( μ : Fin 1 ⊕ Fin d ) :
⟪ ContrMod.stdBasis μ , v ⟫ₘ = η μ μ * v . toFin1dℝ μ := by d : ℕ v : ContrMod d μ : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] v ) = η μ μ * v . toFin1dℝ μ
rw [ as_sum d : ℕ v : ContrMod d μ : Fin 1 ⊕ Fin d ⊢ ( ContrMod.stdBasis μ ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis μ ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η μ μ * v . toFin1dℝ μ d : ℕ v : ContrMod d μ : Fin 1 ⊕ Fin d ⊢ ( ContrMod.stdBasis μ ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis μ ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η μ μ * v . toFin1dℝ μ ] d : ℕ v : ContrMod d μ : Fin 1 ⊕ Fin d ⊢ ( ContrMod.stdBasis μ ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis μ ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η μ μ * v . toFin1dℝ μ
rcases μ with μ | μ inl d : ℕ v : ContrMod d μ : Fin 1 ⊢ ( ContrMod.stdBasis ( Sum.inl μ ) ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl μ ) ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η ( Sum.inl μ ) ( Sum.inl μ ) * v . toFin1dℝ ( Sum.inl μ ) inr d : ℕ v : ContrMod d μ : Fin d ⊢ ( ContrMod.stdBasis ( Sum.inr μ ) ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inr μ ) ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η ( Sum.inr μ ) ( Sum.inr μ ) * v . toFin1dℝ ( Sum.inr μ )
· inl d : ℕ v : ContrMod d μ : Fin 1 ⊢ ( ContrMod.stdBasis ( Sum.inl μ ) ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl μ ) ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η ( Sum.inl μ ) ( Sum.inl μ ) * v . toFin1dℝ ( Sum.inl μ ) fin_cases μ inl.«0» d : ℕ v : ContrMod d ⊢ ( ContrMod.stdBasis ( Sum.inl ( (fun i => i ) ⟨ 0 , ⋯ ⟩ ) ) ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inl ( (fun i => i ) ⟨ 0 , ⋯ ⟩ ) ) ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η ( Sum.inl ( (fun i => i ) ⟨ 0 , ⋯ ⟩ ) ) ( Sum.inl ( (fun i => i ) ⟨ 0 , ⋯ ⟩ ) ) * v . toFin1dℝ ( Sum.inl ( (fun i => i ) ⟨ 0 , ⋯ ⟩ ) )
simp only [ Fin.zero_eta , Fin.isValue , ContrMod.stdBasis_apply_same , one_mul ,
ContrMod.stdBasis_inl_apply_inr , zero_mul , Finset.sum_const_zero , sub_zero , minkowskiMatrix ,
LieAlgebra.Orthogonal.indefiniteDiagonal , diagonal_apply_eq , Sum.elim_inl ] inl.«0» d : ℕ v : ContrMod d ⊢ v . val ( Sum.inl 0 ) = v . toFin1dℝ ( Sum.inl 0 )
rfl All goals completed! 🐙
· inr d : ℕ v : ContrMod d μ : Fin d ⊢ ( ContrMod.stdBasis ( Sum.inr μ ) ) . val ( Sum.inl 0 ) * v . val ( Sum.inl 0 ) -
∑ i , ( ContrMod.stdBasis ( Sum.inr μ ) ) . val ( Sum.inr i ) * v . val ( Sum.inr i ) =
η ( Sum.inr μ ) ( Sum.inr μ ) * v . toFin1dℝ ( Sum.inr μ ) simp only [ Fin.isValue , ContrMod.stdBasis_apply , reduceCtorEq , ↓ reduceIte , zero_mul ,
Sum.inr.injEq , ite_mul , one_mul , Finset.sum_ite_eq , Finset.mem_univ , zero_sub , minkowskiMatrix ,
LieAlgebra.Orthogonal.indefiniteDiagonal , diagonal_apply_eq , Sum.elim_inr , neg_mul , neg_inj ] inr d : ℕ v : ContrMod d μ : Fin d ⊢ v . val ( Sum.inr μ ) = v . toFin1dℝ ( Sum.inr μ )
rfl All goals completed! 🐙
lemma on_basis_mulVec ( μ ν : Fin 1 ⊕ Fin d ) :
⟪ ContrMod.stdBasis μ , Λ *ᵥ ContrMod.stdBasis ν ⟫ₘ = η μ μ * Λ μ ν := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ( Λ *ᵥ ContrMod.stdBasis ν ) ) = η μ μ * Λ μ ν
rw [ basis_left , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * ( Λ *ᵥ ContrMod.stdBasis ν ) . toFin1dℝ μ = η μ μ * Λ μ ν d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * ( Λ *ᵥ ( ContrMod.stdBasis ν ) . toFin1dℝ ) μ = η μ μ * Λ μ ν ContrMod.mulVec_toFin1dℝ d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * ( Λ *ᵥ ( ContrMod.stdBasis ν ) . toFin1dℝ ) μ = η μ μ * Λ μ ν d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * ( Λ *ᵥ ( ContrMod.stdBasis ν ) . toFin1dℝ ) μ = η μ μ * Λ μ ν ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * ( Λ *ᵥ ( ContrMod.stdBasis ν ) . toFin1dℝ ) μ = η μ μ * Λ μ ν
simp [ mulVec , dotProduct , ContrMod.stdBasis_apply , ContrMod.toFin1dℝ_eq_val ] All goals completed! 🐙
lemma on_basis ( μ ν : Fin 1 ⊕ Fin d ) : ⟪ ContrMod.stdBasis μ , ContrMod.stdBasis ν ⟫ₘ = η μ ν := by d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ContrMod.stdBasis ν ) = η μ ν
trans ⟪ ContrMod.stdBasis μ , 1 *ᵥ ContrMod.stdBasis ν ⟫ₘ d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ContrMod.stdBasis ν ) =
contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ( 1 *ᵥ ContrMod.stdBasis ν ) ) d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ( 1 *ᵥ ContrMod.stdBasis ν ) ) = η μ ν
· d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ContrMod.stdBasis ν ) =
contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ( 1 *ᵥ ContrMod.stdBasis ν ) ) rw [ ContrMod.one_mulVec d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ContrMod.stdBasis ν ) =
contrContrContractField ( ContrMod.stdBasis μ ⊗ₜ[ ℝ ] ContrMod.stdBasis ν ) All goals completed! 🐙 ] All goals completed! 🐙
rw [ on_basis_mulVec d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * 1 μ ν = η μ ν d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * 1 μ ν = η μ ν ] d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d ⊢ η μ μ * 1 μ ν = η μ ν
by_cases h : μ = ν pos d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d h : μ = ν ⊢ η μ μ * 1 μ ν = η μ ν neg d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d h : ¬ μ = ν ⊢ η μ μ * 1 μ ν = η μ ν
· pos d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d h : μ = ν ⊢ η μ μ * 1 μ ν = η μ ν subst h pos d : ℕ μ : Fin 1 ⊕ Fin d ⊢ η μ μ * 1 μ μ = η μ μ
simp All goals completed! 🐙
· neg d : ℕ μ : Fin 1 ⊕ Fin d ν : Fin 1 ⊕ Fin d h : ¬ μ = ν ⊢ η μ μ * 1 μ ν = η μ ν simp only [ ne_eq , h , not_false_eq_true , one_apply_ne , mul_zero , off_diag_zero ] All goals completed! 🐙
lemma matrix_apply_stdBasis ( ν μ : Fin 1 ⊕ Fin d ) :
Λ ν μ = η ν ν * ⟪ ContrMod.stdBasis ν , Λ *ᵥ ContrMod.stdBasis μ ⟫ₘ := by d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * contrContrContractField ( ContrMod.stdBasis ν ⊗ₜ[ ℝ ] ( Λ *ᵥ ContrMod.stdBasis μ ) )
rw [ on_basis_mulVec , d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * ( η ν ν * Λ ν μ ) d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * η ν ν * Λ ν μ ← mul_assoc d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * η ν ν * Λ ν μ d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * η ν ν * Λ ν μ ] d : ℕ Λ : Matrix ( Fin 1 ⊕ Fin d ) ( Fin 1 ⊕ Fin d ) ℝ ν : Fin 1 ⊕ Fin d μ : Fin 1 ⊕ Fin d ⊢ Λ ν μ = η ν ν * η ν ν * Λ ν μ
simp [ η_apply_mul_η_apply_diag ν ] All goals completed! 🐙
Self-adjoint
lemma same_eq_det_toSelfAdjoint ( x : ContrMod 3 ) :
⟪ x , x ⟫ₘ = det ( ContrMod.toSelfAdjoint x ) . 1 := by x : ContrMod 3 ⊢ ↑ ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) = (↑ ( ContrMod.toSelfAdjoint x ) ) . det
rw [ ContrMod.toSelfAdjoint_apply_coe , x : ContrMod 3 ⊢ ↑ ( contrContrContractField ( x ⊗ₜ[ ℝ ] x ) ) =
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) ) . det x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 as_sum_toSpace , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) ) . det x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 det_fin_two , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • PauliMatrix.pauliMatrix ( Sum.inl 0 ) -
x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0
PauliMatrix.pauliMatrix , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • PauliMatrix.pauliMatrix ( Sum.inr 0 ) -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 PauliMatrix.pauliMatrix , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] -
x . toFin1dℝ ( Sum.inr 1 ) • PauliMatrix.pauliMatrix ( Sum.inr 1 ) -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 PauliMatrix.pauliMatrix , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • PauliMatrix.pauliMatrix ( Sum.inr 2 ) )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0
PauliMatrix.pauliMatrix , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ x . toSpace , x . toSpace ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 ContrMod.toSpace , x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . toFin1dℝ ( Sum.inl 0 ) • 1 - x . toFin1dℝ ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . toFin1dℝ ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . toFin1dℝ ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0
ContrMod.toFin1dℝ_eq_val x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0 ] x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) * x . val ( Sum.inl 0 ) - ⟪ WithLp.toLp 2 ( x . val ∘ Sum.inr ) , WithLp.toLp 2 ( x . val ∘ Sum.inr ) ⟫_ ℝ ) =
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 0 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 1 -
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
0 1 *
( x . val ( Sum.inl 0 ) • 1 - x . val ( Sum.inr 0 ) • !![ 0 , 1 ; 1 , 0 ] - x . val ( Sum.inr 1 ) • !![ 0 , - I ; I , 0 ] -
x . val ( Sum.inr 2 ) • !![ 1 , 0 ; 0 , - 1 ] )
1 0
simp only [ Fin.isValue , PiLp.inner_apply , Fin.sum_univ_three , ofReal_sub , ofReal_mul , smul_of ,
smul_cons , smul_zero , real_smul , mul_one , smul_empty , smul_neg , Matrix.sub_apply ,
Matrix.smul_apply , one_apply_eq , of_apply , cons_val' , cons_val_zero , cons_val_fin_one , sub_zero ,
cons_val_one , sub_neg_eq_add , ne_eq , zero_ne_one , not_false_eq_true , one_apply_ne , zero_sub ,
one_ne_zero ] x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) ) * ↑ ( x . val ( Sum.inl 0 ) ) -
↑ ( ⟪ ( x . val ∘ Sum.inr ) 0 , ( x . val ∘ Sum.inr ) 0 ⟫_ ℝ + ⟪ ( x . val ∘ Sum.inr ) 1 , ( x . val ∘ Sum.inr ) 1 ⟫_ ℝ +
⟪ ( x . val ∘ Sum.inr ) 2 , ( x . val ∘ Sum.inr ) 2 ⟫_ ℝ ) =
( ↑ ( x . val ( Sum.inl 0 ) ) - ↑ ( x . val ( Sum.inr 2 ) ) ) * ( ↑ ( x . val ( Sum.inl 0 ) ) + ↑ ( x . val ( Sum.inr 2 ) ) ) -
( - ↑ ( x . val ( Sum.inr 0 ) ) + ↑ ( x . val ( Sum.inr 1 ) ) * I ) * ( - ↑ ( x . val ( Sum.inr 0 ) ) - ↑ ( x . val ( Sum.inr 1 ) ) * I )
ring_nf x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) ) ^ 2 -
↑ ( ⟪ ( x . val ∘ Sum.inr ) 0 , ( x . val ∘ Sum.inr ) 0 ⟫_ ℝ + ⟪ ( x . val ∘ Sum.inr ) 1 , ( x . val ∘ Sum.inr ) 1 ⟫_ ℝ +
⟪ ( x . val ∘ Sum.inr ) 2 , ( x . val ∘ Sum.inr ) 2 ⟫_ ℝ ) =
↑ ( x . val ( Sum.inl 0 ) ) ^ 2 - ↑ ( x . val ( Sum.inr 2 ) ) ^ 2 - ↑ ( x . val ( Sum.inr 0 ) ) ^ 2 + ↑ ( x . val ( Sum.inr 1 ) ) ^ 2 * I ^ 2
simp only [ Fin.isValue , Function.comp_apply , inner_self_eq_norm_sq_to_K , Real.norm_eq_abs ,
RCLike.ofReal_real_eq_id , id_eq , sq_abs , ofReal_add , ofReal_pow , I_sq , mul_neg , mul_one ] x : ContrMod 3 ⊢ ↑ ( x . val ( Sum.inl 0 ) ) ^ 2 - ( ↑ ( x . val ( Sum.inr 0 ) ) ^ 2 + ↑ ( x . val ( Sum.inr 1 ) ) ^ 2 + ↑ ( x . val ( Sum.inr 2 ) ) ^ 2 ) =
↑ ( x . val ( Sum.inl 0 ) ) ^ 2 - ↑ ( x . val ( Sum.inr 2 ) ) ^ 2 - ↑ ( x . val ( Sum.inr 0 ) ) ^ 2 + - ↑ ( x . val ( Sum.inr 1 ) ) ^ 2
ring All goals completed! 🐙
The contraction on the basis