Theorem hdmap14lem2a

Description: Prior to part 14 in Baer p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 . (Contributed by NM, 31-May-2015)

	Ref	Expression
Hypotheses	hdmap14lem1a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem1a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem1a.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem1a.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem1a.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem1a.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem1a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem2a.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem1a.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap14lem2a.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hdmap14lem2a.a	$$⊢A={\mathrm{Base}}_P$$
	hdmap14lem1a.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem1a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem3a.x	$$⊢\phi \to X\in V$$
	hdmap14lem1a.f	$$⊢\phi \to F\in B$$
Assertion	hdmap14lem2a	$$⊢\phi \to \exists g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem1a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem1a.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem1a.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem1a.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmap14lem1a.b	$$⊢B={\mathrm{Base}}_R$$
7		hdmap14lem1a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap14lem2a.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hdmap14lem1a.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
10		hdmap14lem2a.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
11		hdmap14lem2a.a	$$⊢A={\mathrm{Base}}_P$$
12		hdmap14lem1a.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
13		hdmap14lem1a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		hdmap14lem3a.x	$$⊢\phi \to X\in V$$
15		hdmap14lem1a.f	$$⊢\phi \to F\in B$$
16		fvoveq1	$$⊢F=0_R\to S\left(F\underset{\dot{}}{·}X\right)=S\left(0_R\underset{\dot{}}{·}X\right)$$
17	16	eqeq1d	$$⊢F=0_R\to \left(S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow S\left(0_R\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
18	17	rexbidv	$$⊢F=0_R\to \left(\exists g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists g\in AS\left(0_R\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
19		difss	$$⊢A\setminus \left\{0_P\right\}\subseteq A$$
20	13	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
21	14	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to X\in V$$
22	15	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to F\in B$$
23		eqid	$$⊢0_R=0_R$$
24		simpr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to F\ne 0_R$$
25	1 2 3 4 5 6 7 8 9 10 11 12 20 21 22 23 24	hdmap14lem1a	$$⊢\left(\phi \wedge F\ne 0_R\right)\to L\left(\left\{S\left(X\right)\right\}\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)$$
26	25	eqcomd	$$⊢\left(\phi \wedge F\ne 0_R\right)\to L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)=L\left(\left\{S\left(X\right)\right\}\right)$$
27		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
28		eqid	$$⊢0_P=0_P$$
29	1 7 13	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
30	1 2 13	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
31	3 5 4 6	lmodvscl	$$⊢\left(U\in \mathrm{LMod}\wedge F\in B\wedge X\in V\right)\to F\underset{\dot{}}{·}X\in V$$
32	30 15 14 31	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}X\in V$$
33	1 2 3 7 27 12 13 32	hdmapcl	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)\in {\mathrm{Base}}_C$$
34	1 2 3 7 27 12 13 14	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_C$$
35	27 10 11 28 8 9 29 33 34	lspsneq	$$⊢\phi \to \left(L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)=L\left(\left\{S\left(X\right)\right\}\right)\leftrightarrow \exists g\in \left(A\setminus \left\{0_P\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
36	35	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to \left(L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)=L\left(\left\{S\left(X\right)\right\}\right)\leftrightarrow \exists g\in \left(A\setminus \left\{0_P\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
37	26 36	mpbid	$$⊢\left(\phi \wedge F\ne 0_R\right)\to \exists g\in \left(A\setminus \left\{0_P\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
38		ssrexv	$$⊢A\setminus \left\{0_P\right\}\subseteq A\to \left(\exists g\in \left(A\setminus \left\{0_P\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\to \exists g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
39	19 37 38	mpsyl	$$⊢\left(\phi \wedge F\ne 0_R\right)\to \exists g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
40	1 7 13	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
41	10 11 28	lmod0cl	$$⊢C\in \mathrm{LMod}\to 0_P\in A$$
42	40 41	syl	$$⊢\phi \to 0_P\in A$$
43		eqid	$$⊢0_U=0_U$$
44		eqid	$$⊢0_C=0_C$$
45	1 2 43 7 44 12 13	hdmapval0	$$⊢\phi \to S\left(0_U\right)=0_C$$
46	3 5 4 23 43	lmod0vs	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to 0_R\underset{\dot{}}{·}X=0_U$$
47	30 14 46	syl2anc	$$⊢\phi \to 0_R\underset{\dot{}}{·}X=0_U$$
48	47	fveq2d	$$⊢\phi \to S\left(0_R\underset{\dot{}}{·}X\right)=S\left(0_U\right)$$
49	27 10 8 28 44	lmod0vs	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(X\right)\in {\mathrm{Base}}_C\right)\to 0_P\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
50	40 34 49	syl2anc	$$⊢\phi \to 0_P\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
51	45 48 50	3eqtr4d	$$⊢\phi \to S\left(0_R\underset{\dot{}}{·}X\right)=0_P\underset{\dot{}}{\bullet }S\left(X\right)$$
52		oveq1	$$⊢g=0_P\to g\underset{\dot{}}{\bullet }S\left(X\right)=0_P\underset{\dot{}}{\bullet }S\left(X\right)$$
53	52	rspceeqv	$$⊢\left(0_P\in A\wedge S\left(0_R\underset{\dot{}}{·}X\right)=0_P\underset{\dot{}}{\bullet }S\left(X\right)\right)\to \exists g\in AS\left(0_R\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
54	42 51 53	syl2anc	$$⊢\phi \to \exists g\in AS\left(0_R\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
55	18 39 54	pm2.61ne	$$⊢\phi \to \exists g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$