hdmapglem7

Description: Lemma for hdmapg . Line 15 in Baer p. 111, f(x,y) alpha = f(y,x). In the proof, our E , ( O{ E } ) , X , Y , k , u , l , and v correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ( ( SY )X ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem7.h	$⊢ H = LHyp (K)$
	hdmapglem7.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapglem7.o	$⊢ O = ocH (K) (W)$
	hdmapglem7.u	$⊢ U = DVecH (K) (W)$
	hdmapglem7.v	$⊢ V = {Base}_{U}$
	hdmapglem7.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmapglem7.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmapglem7.r	$⊢ R = Scalar (U)$
	hdmapglem7.b	$⊢ B = {Base}_{R}$
	hdmapglem7.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	hdmapglem7.n	$⊢ N = LSpan (U)$
	hdmapglem7.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapglem7.x	$⊢ φ \to X \in V$
	hdmapglem7.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hdmapglem7.z	$⊢ \underset{˙}{0} = 0_{R}$
	hdmapglem7.c	$⊢ \underset{˙}{✚} = +_{R}$
	hdmapglem7.s	$⊢ S = HDMap (K) (W)$
	hdmapglem7.g	$⊢ G = HGMap (K) (W)$
	hdmapglem7.y	$⊢ φ \to Y \in V$
Assertion	hdmapglem7	$⊢ φ \to G (S (Y) (X)) = S (X) (Y)$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem7.h	$⊢ H = LHyp (K)$
2		hdmapglem7.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapglem7.o	$⊢ O = ocH (K) (W)$
4		hdmapglem7.u	$⊢ U = DVecH (K) (W)$
5		hdmapglem7.v	$⊢ V = {Base}_{U}$
6		hdmapglem7.p	$⊢ \underset{˙}{+} = +_{U}$
7		hdmapglem7.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
8		hdmapglem7.r	$⊢ R = Scalar (U)$
9		hdmapglem7.b	$⊢ B = {Base}_{R}$
10		hdmapglem7.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
11		hdmapglem7.n	$⊢ N = LSpan (U)$
12		hdmapglem7.k	$⊢ φ \to (K \in HL \land W \in H)$
13		hdmapglem7.x	$⊢ φ \to X \in V$
14		hdmapglem7.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
15		hdmapglem7.z	$⊢ \underset{˙}{0} = 0_{R}$
16		hdmapglem7.c	$⊢ \underset{˙}{✚} = +_{R}$
17		hdmapglem7.s	$⊢ S = HDMap (K) (W)$
18		hdmapglem7.g	$⊢ G = HGMap (K) (W)$
19		hdmapglem7.y	$⊢ φ \to Y \in V$
20	1 2 3 4 5 6 7 8 9 10 11 12 13	hdmapglem7a	$⊢ φ \to \exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
21	1 2 3 4 5 6 7 8 9 10 11 12 19	hdmapglem7a	$⊢ φ \to \exists v \in O (\{E\}) \exists l \in B Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v$
22	12	ad2antrr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to (K \in HL \land W \in H)$
23	1 4 12	dvhlmod	$⊢ φ \to U \in LMod$
24	8	lmodring	$⊢ U \in LMod \to R \in Ring$
25	23 24	syl	$⊢ φ \to R \in Ring$
26	25	ad2antrr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to R \in Ring$
27		simplrr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to k \in B$
28		simprr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to l \in B$
29	1 4 8 9 18 22 28	hgmapcl	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (l) \in B$
30	9 14	ringcl	$⊢ (R \in Ring \land k \in B \land G (l) \in B) \to k \underset{˙}{\times} G (l) \in B$
31	26 27 29 30	syl3anc	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to k \underset{˙}{\times} G (l) \in B$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
34		eqid	$⊢ 0_{U} = 0_{U}$
35	1 32 33 4 5 34 2 12	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
36	35	eldifad	$⊢ φ \to E \in V$
37	36	snssd	$⊢ φ \to \{E\} \subseteq V$
38	1 4 5 3	dochssv	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \subseteq V$
39	12 37 38	syl2anc	$⊢ φ \to O (\{E\}) \subseteq V$
40	39	ad2antrr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to O (\{E\}) \subseteq V$
41		simplrl	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to u \in O (\{E\})$
42	40 41	sseldd	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to u \in V$
43		simprl	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to v \in O (\{E\})$
44	40 43	sseldd	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to v \in V$
45	1 4 5 8 9 17 22 42 44	hdmapipcl	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to S (v) (u) \in B$
46	1 4 8 9 16 18 22 31 45	hgmapadd	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G ((k \underset{˙}{\times} G (l)) \underset{˙}{✚} S (v) (u)) = G (k \underset{˙}{\times} G (l)) \underset{˙}{✚} G (S (v) (u))$
47	1 4 8 9 14 18 22 27 29	hgmapmul	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (k \underset{˙}{\times} G (l)) = G (G (l)) \underset{˙}{\times} G (k)$
48	1 4 8 9 18 22 28	hgmapvv	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (G (l)) = l$
49	48	oveq1d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (G (l)) \underset{˙}{\times} G (k) = l \underset{˙}{\times} G (k)$
50	47 49	eqtrd	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (k \underset{˙}{\times} G (l)) = l \underset{˙}{\times} G (k)$
51		eqid	$⊢ -_{U} = -_{U}$
52	1 2 3 4 5 6 51 7 8 9 14 15 17 18 22 41 43 27 27	hdmapglem5	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (S (v) (u)) = S (u) (v)$
53	50 52	oveq12d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (k \underset{˙}{\times} G (l)) \underset{˙}{✚} G (S (v) (u)) = (l \underset{˙}{\times} G (k)) \underset{˙}{✚} S (u) (v)$
54	46 53	eqtrd	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G ((k \underset{˙}{\times} G (l)) \underset{˙}{✚} S (v) (u)) = (l \underset{˙}{\times} G (k)) \underset{˙}{✚} S (u) (v)$
55	13	ad2antrr	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to X \in V$
56	1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 43 41 28 27	hdmapglem7b	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) = (k \underset{˙}{\times} G (l)) \underset{˙}{✚} S (v) (u)$
57	56	fveq2d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)) = G ((k \underset{˙}{\times} G (l)) \underset{˙}{✚} S (v) (u))$
58	1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 41 43 27 28	hdmapglem7b	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) = (l \underset{˙}{\times} G (k)) \underset{˙}{✚} S (u) (v)$
59	54 57 58	3eqtr4d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B)) \land (v \in O (\{E\}) \land l \in B)) \to G (S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)) = S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) ((l \underset{˙}{\cdot} E) \underset{˙}{+} v)$
60	59	3adantl3	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B)) \to G (S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)) = S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) ((l \underset{˙}{\cdot} E) \underset{˙}{+} v)$
61	60	3adant3	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to G (S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)) = S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) ((l \underset{˙}{\cdot} E) \underset{˙}{+} v)$
62		simp3	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v$
63	62	fveq2d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to S (Y) = S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v)$
64		simp13	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u$
65	63 64	fveq12d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to S (Y) (X) = S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
66	65	fveq2d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to G (S (Y) (X)) = G (S ((l \underset{˙}{\cdot} E) \underset{˙}{+} v) ((k \underset{˙}{\cdot} E) \underset{˙}{+} u))$
67	64	fveq2d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to S (X) = S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u)$
68	67 62	fveq12d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to S (X) (Y) = S ((k \underset{˙}{\cdot} E) \underset{˙}{+} u) ((l \underset{˙}{\cdot} E) \underset{˙}{+} v)$
69	61 66 68	3eqtr4d	$⊢ ((φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \land (v \in O (\{E\}) \land l \in B) \land Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v) \to G (S (Y) (X)) = S (X) (Y)$
70	69	3exp	$⊢ (φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \to ((v \in O (\{E\}) \land l \in B) \to (Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v \to G (S (Y) (X)) = S (X) (Y)))$
71	70	rexlimdvv	$⊢ (φ \land (u \in O (\{E\}) \land k \in B) \land X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u) \to (\exists v \in O (\{E\}) \exists l \in B Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v \to G (S (Y) (X)) = S (X) (Y))$
72	71	3exp	$⊢ φ \to ((u \in O (\{E\}) \land k \in B) \to (X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u \to (\exists v \in O (\{E\}) \exists l \in B Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v \to G (S (Y) (X)) = S (X) (Y))))$
73	72	rexlimdvv	$⊢ φ \to (\exists u \in O (\{E\}) \exists k \in B X = (k \underset{˙}{\cdot} E) \underset{˙}{+} u \to (\exists v \in O (\{E\}) \exists l \in B Y = (l \underset{˙}{\cdot} E) \underset{˙}{+} v \to G (S (Y) (X)) = S (X) (Y)))$
74	20 21 73	mp2d	$⊢ φ \to G (S (Y) (X)) = S (X) (Y)$

Metamath Proof Explorer

Theorem hdmapglem7

Proof