Theorem hdmapglem7b

Description: Lemma for hdmapg . (Contributed by NM, 14-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapglem7.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapglem7.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapglem7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapglem7.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapglem7.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmapglem7.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapglem7.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapglem7.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapglem7.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	hdmapglem7.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmapglem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapglem7.x	$$⊢\phi \to X\in V$$
	hdmapglem7.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmapglem7.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapglem7.c	$$⊢\underset{\dot{}}{✚}={+}_R$$
	hdmapglem7.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapglem7.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hdmapglem7b.u	$$⊢\phi \to x\in O\left(\left\{E\right\}\right)$$
	hdmapglem7b.v	$$⊢\phi \to y\in O\left(\left\{E\right\}\right)$$
	hdmapglem7b.k	$$⊢\phi \to m\in B$$
	hdmapglem7b.l	$$⊢\phi \to n\in B$$
Assertion	hdmapglem7b	$$⊢\phi \to S\left(\left(m\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(n\underset{\dot{}}{\times }G\left(m\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapglem7.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapglem7.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hdmapglem7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hdmapglem7.v	$$⊢V={\mathrm{Base}}_U$$
6		hdmapglem7.p	$$⊢\underset{\dot{}}{+}={+}_U$$
7		hdmapglem7.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
8		hdmapglem7.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
9		hdmapglem7.b	$$⊢B={\mathrm{Base}}_R$$
10		hdmapglem7.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
11		hdmapglem7.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
12		hdmapglem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		hdmapglem7.x	$$⊢\phi \to X\in V$$
14		hdmapglem7.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
15		hdmapglem7.z	$$⊢\underset{\dot{}}{0}=0_R$$
16		hdmapglem7.c	$$⊢\underset{\dot{}}{✚}={+}_R$$
17		hdmapglem7.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
18		hdmapglem7.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
19		hdmapglem7b.u	$$⊢\phi \to x\in O\left(\left\{E\right\}\right)$$
20		hdmapglem7b.v	$$⊢\phi \to y\in O\left(\left\{E\right\}\right)$$
21		hdmapglem7b.k	$$⊢\phi \to m\in B$$
22		hdmapglem7b.l	$$⊢\phi \to n\in B$$
23	1 4 12	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 12	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
28	27	eldifad	$$⊢\phi \to E\in V$$
29	5 8 7 9	lmodvscl	$$⊢\left(U\in \mathrm{LMod}\wedge n\in B\wedge E\in V\right)\to n\underset{\dot{}}{·}E\in V$$
30	23 22 28 29	syl3anc	$$⊢\phi \to n\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	12 31 32	syl2anc	$$⊢\phi \to O\left(\left\{E\right\}\right)\subseteq V$$
34	33 20	sseldd	$$⊢\phi \to y\in V$$
35	5 6	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge n\underset{\dot{}}{·}E\in V\wedge y\in V\right)\to \left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\in V$$
36	23 30 34 35	syl3anc	$$⊢\phi \to \left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\in V$$
37	33 19	sseldd	$$⊢\phi \to x\in V$$
38	1 4 5 6 7 8 9 16 14 17 18 12 36 28 37 21	hdmapgln2	$$⊢\phi \to S\left(\left(m\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(S\left(E\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)\underset{\dot{}}{\times }G\left(m\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)$$
39	1 4 5 6 7 8 9 16 14 17 12 28 34 28 22	hdmapln1	$$⊢\phi \to S\left(E\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(n\underset{\dot{}}{\times }S\left(E\right)\left(E\right)\right)\underset{\dot{}}{✚}S\left(E\right)\left(y\right)$$
40		eqid	$$⊢\mathrm{HVMap}\left(K\right)\left(W\right)=\mathrm{HVMap}\left(K\right)\left(W\right)$$
41		eqid	$$⊢1_R=1_R$$
42	1 2 40 17 12 4 8 41	hdmapevec2	$$⊢\phi \to S\left(E\right)\left(E\right)=1_R$$
43	42	oveq2d	$$⊢\phi \to n\underset{\dot{}}{\times }S\left(E\right)\left(E\right)=n\underset{\dot{}}{\times }{1}_R$$
44	8	lmodring	$$⊢U\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
45	23 44	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
46	9 14 41	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge n\in B\right)\to n\underset{\dot{}}{\times }{1}_R=n$$
47	45 22 46	syl2anc	$$⊢\phi \to n\underset{\dot{}}{\times }{1}_R=n$$
48	43 47	eqtrd	$$⊢\phi \to n\underset{\dot{}}{\times }S\left(E\right)\left(E\right)=n$$
49	1 2 3 4 5 8 9 14 15 17 12 20	hdmapinvlem1	$$⊢\phi \to S\left(E\right)\left(y\right)=\underset{\dot{}}{0}$$
50	48 49	oveq12d	$$⊢\phi \to \left(n\underset{\dot{}}{\times }S\left(E\right)\left(E\right)\right)\underset{\dot{}}{✚}S\left(E\right)\left(y\right)=n\underset{\dot{}}{✚}\underset{\dot{}}{0}$$
51		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
52	45 51	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
53	9 16 15	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge n\in B\right)\to n\underset{\dot{}}{✚}\underset{\dot{}}{0}=n$$
54	52 22 53	syl2anc	$$⊢\phi \to n\underset{\dot{}}{✚}\underset{\dot{}}{0}=n$$
55	39 50 54	3eqtrd	$$⊢\phi \to S\left(E\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=n$$
56	55	oveq1d	$$⊢\phi \to S\left(E\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)\underset{\dot{}}{\times }G\left(m\right)=n\underset{\dot{}}{\times }G\left(m\right)$$
57	1 4 5 6 7 8 9 16 14 17 12 28 34 37 22	hdmapln1	$$⊢\phi \to S\left(x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(n\underset{\dot{}}{\times }S\left(x\right)\left(E\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(y\right)$$
58	1 2 3 4 5 8 9 14 15 17 12 19	hdmapinvlem2	$$⊢\phi \to S\left(x\right)\left(E\right)=\underset{\dot{}}{0}$$
59	58	oveq2d	$$⊢\phi \to n\underset{\dot{}}{\times }S\left(x\right)\left(E\right)=n\underset{\dot{}}{\times }\underset{\dot{}}{0}$$
60	9 14 15	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge n\in B\right)\to n\underset{\dot{}}{\times }\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
61	45 22 60	syl2anc	$$⊢\phi \to n\underset{\dot{}}{\times }\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
62	59 61	eqtrd	$$⊢\phi \to n\underset{\dot{}}{\times }S\left(x\right)\left(E\right)=\underset{\dot{}}{0}$$
63	62	oveq1d	$$⊢\phi \to \left(n\underset{\dot{}}{\times }S\left(x\right)\left(E\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(y\right)=\underset{\dot{}}{0}\underset{\dot{}}{✚}S\left(x\right)\left(y\right)$$
64	1 4 5 8 9 17 12 34 37	hdmapipcl	$$⊢\phi \to S\left(x\right)\left(y\right)\in B$$
65	9 16 15	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge S\left(x\right)\left(y\right)\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{✚}S\left(x\right)\left(y\right)=S\left(x\right)\left(y\right)$$
66	52 64 65	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{✚}S\left(x\right)\left(y\right)=S\left(x\right)\left(y\right)$$
67	57 63 66	3eqtrd	$$⊢\phi \to S\left(x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=S\left(x\right)\left(y\right)$$
68	56 67	oveq12d	$$⊢\phi \to \left(S\left(E\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)\underset{\dot{}}{\times }G\left(m\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(n\underset{\dot{}}{\times }G\left(m\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(y\right)$$
69	38 68	eqtrd	$$⊢\phi \to S\left(\left(m\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}x\right)\left(\left(n\underset{\dot{}}{·}E\right)\underset{\dot{}}{+}y\right)=\left(n\underset{\dot{}}{\times }G\left(m\right)\right)\underset{\dot{}}{✚}S\left(x\right)\left(y\right)$$