Theorem hdmapinvlem3

Description: Line 30 in Baer p. 110, f(sw + u, tw - v) = 0. (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	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}$$

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	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
22		eqid	$$⊢{-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
23	1 4 15	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
24		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
25		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
26		eqid	$$⊢0_U=0_U$$
27	1 24 25 4 5 26 2 15	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
28	27	eldifad	$$⊢\phi \to E\in V$$
29	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$$
30	23 19 28 29	syl3anc	$$⊢\phi \to J\underset{\dot{}}{·}E\in V$$
31	28	snssd	$$⊢\phi \to \left\{E\right\}\subseteq V$$
32	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$$
33	15 31 32	syl2anc	$$⊢\phi \to O\left(\left\{E\right\}\right)\subseteq V$$
34	33 17	sseldd	$$⊢\phi \to D\in V$$
35	1 4 5 7 21 22 13 15 30 34	hdmapsub	$$⊢\phi \to S\left(\left(J\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}D\right)=S\left(J\underset{\dot{}}{·}E\right){-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(D\right)$$
36	35	fveq1d	$$⊢\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)=\left(S\left(J\underset{\dot{}}{·}E\right){-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(D\right)\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)$$
37		eqid	$$⊢{-}_R={-}_R$$
38		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
39	1 4 5 21 38 13 15 30	hdmapcl	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
40	1 4 5 21 38 13 15 34	hdmapcl	$$⊢\phi \to S\left(D\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
41	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$$
42	23 18 28 41	syl3anc	$$⊢\phi \to I\underset{\dot{}}{·}E\in V$$
43	33 16	sseldd	$$⊢\phi \to C\in V$$
44	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$$
45	23 42 43 44	syl3anc	$$⊢\phi \to \left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\in V$$
46	1 4 5 9 37 21 38 22 15 39 40 45	lcdvsubval	$$⊢\phi \to \left(S\left(J\underset{\dot{}}{·}E\right){-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(D\right)\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=S\left(J\underset{\dot{}}{·}E\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right){-}_{R}S\left(D\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)$$
47		eqid	$$⊢{+}_R={+}_R$$
48	1 4 5 6 9 47 13 15 42 43 30	hdmaplna1	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=S\left(J\underset{\dot{}}{·}E\right)\left(I\underset{\dot{}}{·}E\right){+}_{R}S\left(J\underset{\dot{}}{·}E\right)\left(C\right)$$
49	1 4 5 8 9 10 11 13 14 15 42 28 19	hdmapglnm2	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(I\underset{\dot{}}{·}E\right)=S\left(E\right)\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{\times }G\left(J\right)$$
50	1 4 5 8 9 10 11 13 15 28 28 18	hdmaplnm1	$$⊢\phi \to S\left(E\right)\left(I\underset{\dot{}}{·}E\right)=I\underset{\dot{}}{\times }S\left(E\right)\left(E\right)$$
51		eqid	$$⊢\mathrm{HVMap}\left(K\right)\left(W\right)=\mathrm{HVMap}\left(K\right)\left(W\right)$$
52		eqid	$$⊢1_R=1_R$$
53	1 2 51 13 15 4 9 52	hdmapevec2	$$⊢\phi \to S\left(E\right)\left(E\right)=1_R$$
54	53	oveq2d	$$⊢\phi \to I\underset{\dot{}}{\times }S\left(E\right)\left(E\right)=I\underset{\dot{}}{\times }{1}_R$$
55	9	lmodring	$$⊢U\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
56	23 55	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
57	10 11 52	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge I\in B\right)\to I\underset{\dot{}}{\times }{1}_R=I$$
58	56 18 57	syl2anc	$$⊢\phi \to I\underset{\dot{}}{\times }{1}_R=I$$
59	50 54 58	3eqtrd	$$⊢\phi \to S\left(E\right)\left(I\underset{\dot{}}{·}E\right)=I$$
60	59	oveq1d	$$⊢\phi \to S\left(E\right)\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{\times }G\left(J\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
61	49 60	eqtrd	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(I\underset{\dot{}}{·}E\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
62	1 4 5 8 9 10 11 13 14 15 43 28 19	hdmapglnm2	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(C\right)=S\left(E\right)\left(C\right)\underset{\dot{}}{\times }G\left(J\right)$$
63	1 2 3 4 5 9 10 11 12 13 15 16	hdmapinvlem1	$$⊢\phi \to S\left(E\right)\left(C\right)=\underset{\dot{}}{0}$$
64	63	oveq1d	$$⊢\phi \to S\left(E\right)\left(C\right)\underset{\dot{}}{\times }G\left(J\right)=\underset{\dot{}}{0}\underset{\dot{}}{\times }G\left(J\right)$$
65	1 4 9 10 14 15 19	hgmapcl	$$⊢\phi \to G\left(J\right)\in B$$
66	10 11 12	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge G\left(J\right)\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\times }G\left(J\right)=\underset{\dot{}}{0}$$
67	56 65 66	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\times }G\left(J\right)=\underset{\dot{}}{0}$$
68	62 64 67	3eqtrd	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(C\right)=\underset{\dot{}}{0}$$
69	61 68	oveq12d	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(I\underset{\dot{}}{·}E\right){+}_{R}S\left(J\underset{\dot{}}{·}E\right)\left(C\right)=\left(I\underset{\dot{}}{\times }G\left(J\right)\right){+}_R\underset{\dot{}}{0}$$
70		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
71	56 70	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
72	9 10 11	lmodmcl	$$⊢\left(U\in \mathrm{LMod}\wedge I\in B\wedge G\left(J\right)\in B\right)\to I\underset{\dot{}}{\times }G\left(J\right)\in B$$
73	23 18 65 72	syl3anc	$$⊢\phi \to I\underset{\dot{}}{\times }G\left(J\right)\in B$$
74	10 47 12	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge I\underset{\dot{}}{\times }G\left(J\right)\in B\right)\to \left(I\underset{\dot{}}{\times }G\left(J\right)\right){+}_R\underset{\dot{}}{0}=I\underset{\dot{}}{\times }G\left(J\right)$$
75	71 73 74	syl2anc	$$⊢\phi \to \left(I\underset{\dot{}}{\times }G\left(J\right)\right){+}_R\underset{\dot{}}{0}=I\underset{\dot{}}{\times }G\left(J\right)$$
76	48 69 75	3eqtrd	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
77	1 4 5 6 9 47 13 15 42 43 34	hdmaplna1	$$⊢\phi \to S\left(D\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=S\left(D\right)\left(I\underset{\dot{}}{·}E\right){+}_{R}S\left(D\right)\left(C\right)$$
78	1 4 5 8 9 10 11 13 15 28 34 18	hdmaplnm1	$$⊢\phi \to S\left(D\right)\left(I\underset{\dot{}}{·}E\right)=I\underset{\dot{}}{\times }S\left(D\right)\left(E\right)$$
79	1 2 3 4 5 9 10 11 12 13 15 17	hdmapinvlem2	$$⊢\phi \to S\left(D\right)\left(E\right)=\underset{\dot{}}{0}$$
80	79	oveq2d	$$⊢\phi \to I\underset{\dot{}}{\times }S\left(D\right)\left(E\right)=I\underset{\dot{}}{\times }\underset{\dot{}}{0}$$
81	10 11 12	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge I\in B\right)\to I\underset{\dot{}}{\times }\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
82	56 18 81	syl2anc	$$⊢\phi \to I\underset{\dot{}}{\times }\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
83	78 80 82	3eqtrrd	$$⊢\phi \to \underset{\dot{}}{0}=S\left(D\right)\left(I\underset{\dot{}}{·}E\right)$$
84	83 20	oveq12d	$$⊢\phi \to \underset{\dot{}}{0}{+}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)=S\left(D\right)\left(I\underset{\dot{}}{·}E\right){+}_{R}S\left(D\right)\left(C\right)$$
85	10 47 12	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge I\underset{\dot{}}{\times }G\left(J\right)\in B\right)\to \underset{\dot{}}{0}{+}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
86	71 73 85	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{+}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
87	77 84 86	3eqtr2d	$$⊢\phi \to S\left(D\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=I\underset{\dot{}}{\times }G\left(J\right)$$
88	76 87	oveq12d	$$⊢\phi \to S\left(J\underset{\dot{}}{·}E\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right){-}_{R}S\left(D\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=\left(I\underset{\dot{}}{\times }G\left(J\right)\right){-}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)$$
89	46 88	eqtrd	$$⊢\phi \to \left(S\left(J\underset{\dot{}}{·}E\right){-}_{\mathrm{LCDual}\left(K\right)\left(W\right)}S\left(D\right)\right)\left(\left(I\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}C\right)=\left(I\underset{\dot{}}{\times }G\left(J\right)\right){-}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)$$
90	10 12 37	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge I\underset{\dot{}}{\times }G\left(J\right)\in B\right)\to \left(I\underset{\dot{}}{\times }G\left(J\right)\right){-}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)=\underset{\dot{}}{0}$$
91	71 73 90	syl2anc	$$⊢\phi \to \left(I\underset{\dot{}}{\times }G\left(J\right)\right){-}_R\left(I\underset{\dot{}}{\times }G\left(J\right)\right)=\underset{\dot{}}{0}$$
92	36 89 91	3eqtrd	$$⊢\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}$$