Theorem hdmap14lem2N

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

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

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem3.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap14lem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmap14lem1.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmap14lem1.z	$$⊢Z=0_R$$
9		hdmap14lem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
10		hdmap14lem2.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
11		hdmap14lem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
12		hdmap14lem2.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
13		hdmap14lem2.a	$$⊢A={\mathrm{Base}}_P$$
14		hdmap14lem2.q	$$⊢Q=0_P$$
15		hdmap14lem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
16		hdmap14lem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hdmap14lem3.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		hdmap14lem1.f	$$⊢\phi \to F\in \left(B\setminus \left\{Z\right\}\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmap14lem1	$$⊢\phi \to L\left(\left\{S\left(X\right)\right\}\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)$$
20	19	eqcomd	$$⊢\phi \to L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)=L\left(\left\{S\left(X\right)\right\}\right)$$
21		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
22	1 9 16	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
23	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
24	18	eldifad	$$⊢\phi \to F\in B$$
25	17	eldifad	$$⊢\phi \to X\in V$$
26	3 6 4 7	lmodvscl	$$⊢\left(U\in \mathrm{LMod}\wedge F\in B\wedge X\in V\right)\to F\underset{\dot{}}{·}X\in V$$
27	23 24 25 26	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}X\in V$$
28	1 2 3 9 21 15 16 27	hdmapcl	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)\in {\mathrm{Base}}_C$$
29	1 2 3 9 21 15 16 25	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_C$$
30	21 12 13 14 10 11 22 28 29	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\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
31	20 30	mpbid	$$⊢\phi \to \exists g\in \left(A\setminus \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$