Metamath Proof Explorer

Theorem nvinv

Description: Minus 1 times a vector is the underlying group's inverse element. Equation 2 of Kreyszig p. 51. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvinv.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		nvinv.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
		nvinv.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
		nvinv.5	⊢ 𝑀 = ( inv ‘ 𝐺 )
	Assertion	nvinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nvinv.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvinv.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
3		nvinv.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
4		nvinv.5	⊢ 𝑀 = ( inv ‘ 𝐺 )
5		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
6	5	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
7	2	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
8	3	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
9	1 2	bafval	⊢ 𝑋 = ran 𝐺
10	7 8 9 4	vcm	⊢ ( ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )
11	6 10	sylan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )