Metamath Proof Explorer

Theorem vcm

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

Ref Expression
Hypotheses vcm.1 ⊢ 𝐺 = ( 1st ‘ 𝑊 )
vcm.2 ⊢ 𝑆 = ( 2nd ‘ 𝑊 )
vcm.3 ⊢ 𝑋 = ran 𝐺
vcm.4 ⊢ 𝑀 = ( inv ‘ 𝐺 )
Assertion vcm ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 vcm.1 ⊢ 𝐺 = ( 1st ‘ 𝑊 )
2 vcm.2 ⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3 vcm.3 ⊢ 𝑋 = ran 𝐺
4 vcm.4 ⊢ 𝑀 = ( inv ‘ 𝐺 )
5 1 vcgrp ⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp )
6 5 adantr ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
7 neg1cn ⊢ - 1 ∈ ℂ
8 1 2 3 vccl ⊢ ( ( 𝑊 ∈ CVecOLD ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
9 7 8 mp3an2 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
10 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
11 3 10 grporid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( GId ‘ 𝐺 ) ) = ( - 1 𝑆 𝐴 ) )
12 6 9 11 syl2anc ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( GId ‘ 𝐺 ) ) = ( - 1 𝑆 𝐴 ) )
13 simpr ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
14 3 4 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ 𝑋 )
15 5 14 sylan ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ 𝑋 )
16 3 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( - 1 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑀 ‘ 𝐴 ) ∈ 𝑋 ) ) → ( ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) ) )
17 6 9 13 15 16 syl13anc ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) ) )
18 1 2 3 vcidOLD ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
19 18 oveq2d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) )
20 ax-1cn ⊢ 1 ∈ ℂ
21 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
22 20 7 21 addcomli ⊢ ( - 1 + 1 ) = 0
23 22 oveq1i ⊢ ( ( - 1 + 1 ) 𝑆 𝐴 ) = ( 0 𝑆 𝐴 )
24 1 2 3 vcdir ⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( - 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( - 1 + 1 ) 𝑆 𝐴 ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
25 7 24 mp3anr1 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( - 1 + 1 ) 𝑆 𝐴 ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
26 20 25 mpanr1 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 + 1 ) 𝑆 𝐴 ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) )
27 1 2 3 10 vc0 ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 0 𝑆 𝐴 ) = ( GId ‘ 𝐺 ) )
28 23 26 27 3eqtr3a ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( GId ‘ 𝐺 ) )
29 19 28 eqtr3d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) = ( GId ‘ 𝐺 ) )
30 29 oveq1d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( ( - 1 𝑆 𝐴 ) 𝐺 𝐴 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) )
31 17 30 eqtr3d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) ) = ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) )
32 3 10 4 grporinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
33 5 32 sylan ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( GId ‘ 𝐺 ) )
34 33 oveq2d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( 𝐴 𝐺 ( 𝑀 ‘ 𝐴 ) ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( GId ‘ 𝐺 ) ) )
35 31 34 eqtr3d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( ( - 1 𝑆 𝐴 ) 𝐺 ( GId ‘ 𝐺 ) ) )
36 3 10 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑀 ‘ 𝐴 ) ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) )
37 6 15 36 syl2anc ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ 𝐴 ) )
38 35 37 eqtr3d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐴 ) 𝐺 ( GId ‘ 𝐺 ) ) = ( 𝑀 ‘ 𝐴 ) )
39 12 38 eqtr3d ⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )