hdmapinvlem4

Description: Part 1.1 of Proposition 1 of Baer p. 110. We use C , D , I , and J for Baer's u, v, s, and t. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SD )C ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem3.h	$⊢ H = LHyp (K)$
	hdmapinvlem3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapinvlem3.o	$⊢ O = ocH (K) (W)$
	hdmapinvlem3.u	$⊢ U = DVecH (K) (W)$
	hdmapinvlem3.v	$⊢ V = {Base}_{U}$
	hdmapinvlem3.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmapinvlem3.m	$⊢ \underset{˙}{-} = -_{U}$
	hdmapinvlem3.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmapinvlem3.r	$⊢ R = Scalar (U)$
	hdmapinvlem3.b	$⊢ B = {Base}_{R}$
	hdmapinvlem3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hdmapinvlem3.z	$⊢ \underset{˙}{0} = 0_{R}$
	hdmapinvlem3.s	$⊢ S = HDMap (K) (W)$
	hdmapinvlem3.g	$⊢ G = HGMap (K) (W)$
	hdmapinvlem3.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapinvlem3.c	$⊢ φ \to C \in O (\{E\})$
	hdmapinvlem3.d	$⊢ φ \to D \in O (\{E\})$
	hdmapinvlem3.i	$⊢ φ \to I \in B$
	hdmapinvlem3.j	$⊢ φ \to J \in B$
	hdmapinvlem3.ij	$⊢ φ \to I \underset{˙}{\times} G (J) = S (D) (C)$
Assertion	hdmapinvlem4	$⊢ φ \to J \underset{˙}{\times} G (I) = S (C) (D)$

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem3.h	$⊢ H = LHyp (K)$
2		hdmapinvlem3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapinvlem3.o	$⊢ O = ocH (K) (W)$
4		hdmapinvlem3.u	$⊢ U = DVecH (K) (W)$
5		hdmapinvlem3.v	$⊢ V = {Base}_{U}$
6		hdmapinvlem3.p	$⊢ \underset{˙}{+} = +_{U}$
7		hdmapinvlem3.m	$⊢ \underset{˙}{-} = -_{U}$
8		hdmapinvlem3.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
9		hdmapinvlem3.r	$⊢ R = Scalar (U)$
10		hdmapinvlem3.b	$⊢ B = {Base}_{R}$
11		hdmapinvlem3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
12		hdmapinvlem3.z	$⊢ \underset{˙}{0} = 0_{R}$
13		hdmapinvlem3.s	$⊢ S = HDMap (K) (W)$
14		hdmapinvlem3.g	$⊢ G = HGMap (K) (W)$
15		hdmapinvlem3.k	$⊢ φ \to (K \in HL \land W \in H)$
16		hdmapinvlem3.c	$⊢ φ \to C \in O (\{E\})$
17		hdmapinvlem3.d	$⊢ φ \to D \in O (\{E\})$
18		hdmapinvlem3.i	$⊢ φ \to I \in B$
19		hdmapinvlem3.j	$⊢ φ \to J \in B$
20		hdmapinvlem3.ij	$⊢ φ \to I \underset{˙}{\times} G (J) = S (D) (C)$
21		eqid	$⊢ -_{R} = -_{R}$
22	1 4 15	dvhlmod	$⊢ φ \to U \in LMod$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
25		eqid	$⊢ 0_{U} = 0_{U}$
26	1 23 24 4 5 25 2 15	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
27	26	eldifad	$⊢ φ \to E \in V$
28	5 9 8 10	lmodvscl	$⊢ (U \in LMod \land J \in B \land E \in V) \to J \underset{˙}{\cdot} E \in V$
29	22 19 27 28	syl3anc	$⊢ φ \to J \underset{˙}{\cdot} E \in V$
30	27	snssd	$⊢ φ \to \{E\} \subseteq V$
31	1 4 5 3	dochssv	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \subseteq V$
32	15 30 31	syl2anc	$⊢ φ \to O (\{E\}) \subseteq V$
33	32 17	sseldd	$⊢ φ \to D \in V$
34	5 9 8 10	lmodvscl	$⊢ (U \in LMod \land I \in B \land E \in V) \to I \underset{˙}{\cdot} E \in V$
35	22 18 27 34	syl3anc	$⊢ φ \to I \underset{˙}{\cdot} E \in V$
36	32 16	sseldd	$⊢ φ \to C \in V$
37	5 6	lmodvacl	$⊢ (U \in LMod \land I \underset{˙}{\cdot} E \in V \land C \in V) \to (I \underset{˙}{\cdot} E) \underset{˙}{+} C \in V$
38	22 35 36 37	syl3anc	$⊢ φ \to (I \underset{˙}{\cdot} E) \underset{˙}{+} C \in V$
39	1 4 5 7 9 21 13 15 29 33 38	hdmaplns1	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) = S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (J \underset{˙}{\cdot} E) -_{R} S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (D)$
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	hdmapinvlem3	$⊢ φ \to S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = \underset{˙}{0}$
41	5 7	lmodvsubcl	$⊢ (U \in LMod \land J \underset{˙}{\cdot} E \in V \land D \in V) \to (J \underset{˙}{\cdot} E) \underset{˙}{-} D \in V$
42	22 29 33 41	syl3anc	$⊢ φ \to (J \underset{˙}{\cdot} E) \underset{˙}{-} D \in V$
43	1 4 5 9 12 13 15 42 38	hdmapip0com	$⊢ φ \to (S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = \underset{˙}{0} \leftrightarrow S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) = \underset{˙}{0})$
44	40 43	mpbid	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) = \underset{˙}{0}$
45	1 4 5 8 9 10 11 13 15 27 38 19	hdmaplnm1	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (J \underset{˙}{\cdot} E) = J \underset{˙}{\times} S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (E)$
46		eqid	$⊢ +_{R} = +_{R}$
47	1 4 5 6 9 46 13 15 27 35 36	hdmaplna2	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (E) = S (I \underset{˙}{\cdot} E) (E) +_{R} S (C) (E)$
48	1 2 3 4 5 9 10 11 12 13 15 16	hdmapinvlem2	$⊢ φ \to S (C) (E) = \underset{˙}{0}$
49	48	oveq2d	$⊢ φ \to S (I \underset{˙}{\cdot} E) (E) +_{R} S (C) (E) = S (I \underset{˙}{\cdot} E) (E) +_{R} \underset{˙}{0}$
50	9	lmodring	$⊢ U \in LMod \to R \in Ring$
51	22 50	syl	$⊢ φ \to R \in Ring$
52		ringgrp	$⊢ R \in Ring \to R \in Grp$
53	51 52	syl	$⊢ φ \to R \in Grp$
54	1 4 5 9 10 13 15 27 35	hdmapipcl	$⊢ φ \to S (I \underset{˙}{\cdot} E) (E) \in B$
55	10 46 12	grprid	$⊢ (R \in Grp \land S (I \underset{˙}{\cdot} E) (E) \in B) \to S (I \underset{˙}{\cdot} E) (E) +_{R} \underset{˙}{0} = S (I \underset{˙}{\cdot} E) (E)$
56	53 54 55	syl2anc	$⊢ φ \to S (I \underset{˙}{\cdot} E) (E) +_{R} \underset{˙}{0} = S (I \underset{˙}{\cdot} E) (E)$
57	1 4 5 8 9 10 11 13 14 15 27 27 18	hdmapglnm2	$⊢ φ \to S (I \underset{˙}{\cdot} E) (E) = S (E) (E) \underset{˙}{\times} G (I)$
58		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
59		eqid	$⊢ 1_{R} = 1_{R}$
60	1 2 58 13 15 4 9 59	hdmapevec2	$⊢ φ \to S (E) (E) = 1_{R}$
61	60	oveq1d	$⊢ φ \to S (E) (E) \underset{˙}{\times} G (I) = 1_{R} \underset{˙}{\times} G (I)$
62	1 4 9 10 14 15 18	hgmapcl	$⊢ φ \to G (I) \in B$
63	10 11 59	ringlidm	$⊢ (R \in Ring \land G (I) \in B) \to 1_{R} \underset{˙}{\times} G (I) = G (I)$
64	51 62 63	syl2anc	$⊢ φ \to 1_{R} \underset{˙}{\times} G (I) = G (I)$
65	61 64	eqtrd	$⊢ φ \to S (E) (E) \underset{˙}{\times} G (I) = G (I)$
66	56 57 65	3eqtrd	$⊢ φ \to S (I \underset{˙}{\cdot} E) (E) +_{R} \underset{˙}{0} = G (I)$
67	47 49 66	3eqtrd	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (E) = G (I)$
68	67	oveq2d	$⊢ φ \to J \underset{˙}{\times} S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (E) = J \underset{˙}{\times} G (I)$
69	45 68	eqtrd	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (J \underset{˙}{\cdot} E) = J \underset{˙}{\times} G (I)$
70	1 4 5 6 9 46 13 15 33 35 36	hdmaplna2	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (D) = S (I \underset{˙}{\cdot} E) (D) +_{R} S (C) (D)$
71	1 4 5 8 9 10 11 13 14 15 33 27 18	hdmapglnm2	$⊢ φ \to S (I \underset{˙}{\cdot} E) (D) = S (E) (D) \underset{˙}{\times} G (I)$
72	1 2 3 4 5 9 10 11 12 13 15 17	hdmapinvlem1	$⊢ φ \to S (E) (D) = \underset{˙}{0}$
73	72	oveq1d	$⊢ φ \to S (E) (D) \underset{˙}{\times} G (I) = \underset{˙}{0} \underset{˙}{\times} G (I)$
74	10 11 12	ringlz	$⊢ (R \in Ring \land G (I) \in B) \to \underset{˙}{0} \underset{˙}{\times} G (I) = \underset{˙}{0}$
75	51 62 74	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\times} G (I) = \underset{˙}{0}$
76	71 73 75	3eqtrd	$⊢ φ \to S (I \underset{˙}{\cdot} E) (D) = \underset{˙}{0}$
77	76	oveq1d	$⊢ φ \to S (I \underset{˙}{\cdot} E) (D) +_{R} S (C) (D) = \underset{˙}{0} +_{R} S (C) (D)$
78	1 4 5 9 10 13 15 33 36	hdmapipcl	$⊢ φ \to S (C) (D) \in B$
79	10 46 12	grplid	$⊢ (R \in Grp \land S (C) (D) \in B) \to \underset{˙}{0} +_{R} S (C) (D) = S (C) (D)$
80	53 78 79	syl2anc	$⊢ φ \to \underset{˙}{0} +_{R} S (C) (D) = S (C) (D)$
81	70 77 80	3eqtrd	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (D) = S (C) (D)$
82	69 81	oveq12d	$⊢ φ \to S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (J \underset{˙}{\cdot} E) -_{R} S ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) (D) = (J \underset{˙}{\times} G (I)) -_{R} S (C) (D)$
83	39 44 82	3eqtr3rd	$⊢ φ \to (J \underset{˙}{\times} G (I)) -_{R} S (C) (D) = \underset{˙}{0}$
84	9 10 11	lmodmcl	$⊢ (U \in LMod \land J \in B \land G (I) \in B) \to J \underset{˙}{\times} G (I) \in B$
85	22 19 62 84	syl3anc	$⊢ φ \to J \underset{˙}{\times} G (I) \in B$
86	10 12 21	grpsubeq0	$⊢ (R \in Grp \land J \underset{˙}{\times} G (I) \in B \land S (C) (D) \in B) \to ((J \underset{˙}{\times} G (I)) -_{R} S (C) (D) = \underset{˙}{0} \leftrightarrow J \underset{˙}{\times} G (I) = S (C) (D))$
87	53 85 78 86	syl3anc	$⊢ φ \to ((J \underset{˙}{\times} G (I)) -_{R} S (C) (D) = \underset{˙}{0} \leftrightarrow J \underset{˙}{\times} G (I) = S (C) (D))$
88	83 87	mpbid	$⊢ φ \to J \underset{˙}{\times} G (I) = S (C) (D)$

Metamath Proof Explorer

Theorem hdmapinvlem4

Proof