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 ⊢ G = 1 st ⁡ W
vcm.2 ⊢ S = 2 nd ⁡ W
vcm.3 ⊢ X = ran ⁡ G
vcm.4 ⊢ M = inv ⁡ G
Assertion vcm ⊢ W ∈ CVec OLD ∧ A ∈ X → -1 S A = M ⁡ A

Proof

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