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 \in {CVec}_{OLD} \land A \in X) \to -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 \in {CVec}_{OLD} \to G \in GrpOp$
6	5	adantr	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to G \in GrpOp$
7		neg1cn	$⊢ - 1 \in ℂ$
8	1 2 3	vccl	$⊢ (W \in {CVec}_{OLD} \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
9	7 8	mp3an2	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to -1 S A \in X$
10		eqid	$⊢ GId (G) = GId (G)$
11	3 10	grporid	$⊢ (G \in GrpOp \land -1 S A \in X) \to (-1 S A) G GId (G) = -1 S A$
12	6 9 11	syl2anc	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G GId (G) = -1 S A$
13		simpr	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to A \in X$
14	3 4	grpoinvcl	$⊢ (G \in GrpOp \land A \in X) \to M (A) \in X$
15	5 14	sylan	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to M (A) \in X$
16	3	grpoass	$⊢ (G \in GrpOp \land (-1 S A \in X \land A \in X \land M (A) \in X)) \to ((-1 S A) G A) G M (A) = (-1 S A) G (A G M (A))$
17	6 9 13 15 16	syl13anc	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to ((-1 S A) G A) G M (A) = (-1 S A) G (A G M (A))$
18	1 2 3	vcidOLD	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to 1 S A = A$
19	18	oveq2d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G (1 S A) = (-1 S A) G A$
20		ax-1cn	$⊢ 1 \in ℂ$
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 \in {CVec}_{OLD} \land (- 1 \in ℂ \land 1 \in ℂ \land A \in X)) \to (- 1 + 1) S A = (-1 S A) G (1 S A)$
25	7 24	mp3anr1	$⊢ (W \in {CVec}_{OLD} \land (1 \in ℂ \land A \in X)) \to (- 1 + 1) S A = (-1 S A) G (1 S A)$
26	20 25	mpanr1	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (- 1 + 1) S A = (-1 S A) G (1 S A)$
27	1 2 3 10	vc0	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to 0 S A = GId (G)$
28	23 26 27	3eqtr3a	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G (1 S A) = GId (G)$
29	19 28	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G A = GId (G)$
30	29	oveq1d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to ((-1 S A) G A) G M (A) = GId (G) G M (A)$
31	17 30	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G (A G M (A)) = GId (G) G M (A)$
32	3 10 4	grporinv	$⊢ (G \in GrpOp \land A \in X) \to A G M (A) = GId (G)$
33	5 32	sylan	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to A G M (A) = GId (G)$
34	33	oveq2d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G (A G M (A)) = (-1 S A) G GId (G)$
35	31 34	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to GId (G) G M (A) = (-1 S A) G GId (G)$
36	3 10	grpolid	$⊢ (G \in GrpOp \land M (A) \in X) \to GId (G) G M (A) = M (A)$
37	6 15 36	syl2anc	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to GId (G) G M (A) = M (A)$
38	35 37	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (-1 S A) G GId (G) = M (A)$
39	12 38	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to -1 S A = M (A)$

Metamath Proof Explorer

Theorem vcm

Proof