Theorem 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=\mathrm{LHyp}\left(K\right)$$
	hdmapinvlem3.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapinvlem3.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapinvlem3.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapinvlem3.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapinvlem3.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmapinvlem3.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmapinvlem3.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapinvlem3.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapinvlem3.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapinvlem3.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmapinvlem3.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapinvlem3.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapinvlem3.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hdmapinvlem3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapinvlem3.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
	hdmapinvlem3.d	$$⊢\phi \to D\in O\left(\left\{E\right\}\right)$$
	hdmapinvlem3.i	$$⊢\phi \to I\in B$$
	hdmapinvlem3.j	$$⊢\phi \to J\in B$$
	hdmapinvlem3.ij	$$⊢\phi \to I\underset{\dot{}}{\times }G\left(J\right)=S\left(D\right)\left(C\right)$$
Assertion	hdmapinvlem4	$$⊢\phi \to J\underset{\dot{}}{\times }G\left(I\right)=S\left(C\right)\left(D\right)$$

Proof

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