Theorem hdmap14lem3

Description: Prior to part 14 in Baer p. 49, line 26. (Contributed by NM, 31-May-2015)

	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	hdmap14lem3	$$⊢\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		eqid	$$⊢0_C=0_C$$
23	1 9 16	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
24	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
25	18	eldifad	$$⊢\phi \to F\in B$$
26	17	eldifad	$$⊢\phi \to X\in V$$
27	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$$
28	24 25 26 27	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}X\in V$$
29	1 2 3 9 21 15 16 28	hdmapcl	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)\in {\mathrm{Base}}_C$$
30	1 2 3 5 9 22 21 15 16 17	hdmapnzcl	$$⊢\phi \to S\left(X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
31	21 12 13 14 10 22 11 23 29 30	lspsneu	$$⊢\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)$$
32	20 31	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)$$