Theorem hdmap14lem13

Description: Lemma for proof of part 14 in Baer p. 50. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem12.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem12.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem12.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem12.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem12.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem12.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem12.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem12.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem12.f	$$⊢\phi \to F\in B$$
	hdmap14lem12.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hdmap14lem12.a	$$⊢A={\mathrm{Base}}_P$$
	hdmap14lem12.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap14lem12.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap14lem12.g	$$⊢\phi \to G\in A$$
Assertion	hdmap14lem13	$$⊢\phi \to \left(S\left(F\underset{\dot{}}{·}X\right)=G\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \forall y\in VS\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem12.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem12.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem12.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem12.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmap14lem12.b	$$⊢B={\mathrm{Base}}_R$$
7		hdmap14lem12.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap14lem12.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hdmap14lem12.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hdmap14lem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		hdmap14lem12.f	$$⊢\phi \to F\in B$$
12		hdmap14lem12.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
13		hdmap14lem12.a	$$⊢A={\mathrm{Base}}_P$$
14		hdmap14lem12.o	$$⊢\underset{\dot{}}{0}=0_U$$
15		hdmap14lem12.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap14lem12.g	$$⊢\phi \to G\in A$$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	hdmap14lem12	$$⊢\phi \to \left(S\left(F\underset{\dot{}}{·}X\right)=G\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
18		velsn	$$⊢y\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow y=\underset{\dot{}}{0}$$
19	1 7 10	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
20		eqid	$$⊢0_C=0_C$$
21	12 8 13 20	lmodvs0	$$⊢\left(C\in \mathrm{LMod}\wedge G\in A\right)\to G\underset{\dot{}}{\bullet }{0}_C=0_C$$
22	19 16 21	syl2anc	$$⊢\phi \to G\underset{\dot{}}{\bullet }{0}_C=0_C$$
23	1 2 14 7 20 9 10	hdmapval0	$$⊢\phi \to S\left(\underset{\dot{}}{0}\right)=0_C$$
24	23	oveq2d	$$⊢\phi \to G\underset{\dot{}}{\bullet }S\left(\underset{\dot{}}{0}\right)=G\underset{\dot{}}{\bullet }{0}_C$$
25	1 2 10	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
26	5 4 6 14	lmodvs0	$$⊢\left(U\in \mathrm{LMod}\wedge F\in B\right)\to F\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
27	25 11 26	syl2anc	$$⊢\phi \to F\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
28	27	fveq2d	$$⊢\phi \to S\left(F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=S\left(\underset{\dot{}}{0}\right)$$
29	28 23	eqtrd	$$⊢\phi \to S\left(F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=0_C$$
30	22 24 29	3eqtr4rd	$$⊢\phi \to S\left(F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=G\underset{\dot{}}{\bullet }S\left(\underset{\dot{}}{0}\right)$$
31		oveq2	$$⊢y=\underset{\dot{}}{0}\to F\underset{\dot{}}{·}y=F\underset{\dot{}}{·}\underset{\dot{}}{0}$$
32	31	fveq2d	$$⊢y=\underset{\dot{}}{0}\to S\left(F\underset{\dot{}}{·}y\right)=S\left(F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$
33		fveq2	$$⊢y=\underset{\dot{}}{0}\to S\left(y\right)=S\left(\underset{\dot{}}{0}\right)$$
34	33	oveq2d	$$⊢y=\underset{\dot{}}{0}\to G\underset{\dot{}}{\bullet }S\left(y\right)=G\underset{\dot{}}{\bullet }S\left(\underset{\dot{}}{0}\right)$$
35	32 34	eqeq12d	$$⊢y=\underset{\dot{}}{0}\to \left(S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\leftrightarrow S\left(F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=G\underset{\dot{}}{\bullet }S\left(\underset{\dot{}}{0}\right)\right)$$
36	30 35	syl5ibrcom	$$⊢\phi \to \left(y=\underset{\dot{}}{0}\to S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
37	18 36	syl5bi	$$⊢\phi \to \left(y\in \left\{\underset{\dot{}}{0}\right\}\to S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
38	37	ralrimiv	$$⊢\phi \to \forall y\in \left\{\underset{\dot{}}{0}\right\}S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)$$
39	38	biantrud	$$⊢\phi \to \left(\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\leftrightarrow \left(\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\wedge \forall y\in \left\{\underset{\dot{}}{0}\right\}S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)\right)$$
40		ralunb	$$⊢\forall y\in \left(\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\leftrightarrow \left(\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\wedge \forall y\in \left\{\underset{\dot{}}{0}\right\}S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
41	39 40	bitr4di	$$⊢\phi \to \left(\forall y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\leftrightarrow \forall y\in \left(\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
42	3 14	lmod0vcl	$$⊢U\in \mathrm{LMod}\to \underset{\dot{}}{0}\in V$$
43		difsnid	$$⊢\underset{\dot{}}{0}\in V\to \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\cup \left\{\underset{\dot{}}{0}\right\}=V$$
44	25 42 43	3syl	$$⊢\phi \to \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\cup \left\{\underset{\dot{}}{0}\right\}=V$$
45	44	raleqdv	$$⊢\phi \to \left(\forall y\in \left(\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)S\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\leftrightarrow \forall y\in VS\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$
46	17 41 45	3bitrd	$$⊢\phi \to \left(S\left(F\underset{\dot{}}{·}X\right)=G\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \forall y\in VS\left(F\underset{\dot{}}{·}y\right)=G\underset{\dot{}}{\bullet }S\left(y\right)\right)$$