Theorem hdmap14lem1a

Description: Prior to part 14 in Baer p. 49, line 25. (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$$
	hdmap14lem1a.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmap14lem1a.fn	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
Assertion	hdmap14lem1a	$$⊢\phi \to L\left(\left\{S\left(X\right)\right\}\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\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		hdmap14lem1a.z	$$⊢\underset{\dot{}}{0}=0_R$$
17		hdmap14lem1a.fn	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
18	1 2 13	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
19		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
20	3 5 4 6 16 19	lspsnvs	$$⊢\left(U\in \mathrm{LVec}\wedge \left(F\in B\wedge F\ne \underset{\dot{}}{0}\right)\wedge X\in V\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{F\underset{\dot{}}{·}X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
21	18 15 17 14 20	syl121anc	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{F\underset{\dot{}}{·}X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
22	21	fveq2d	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{F\underset{\dot{}}{·}X\right\}\right)\right)=\mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)$$
23		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
24	1 2 13	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
25	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$$
26	24 15 14 25	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}X\in V$$
27	1 2 3 19 7 9 23 12 13 26	hdmap10	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{F\underset{\dot{}}{·}X\right\}\right)\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)$$
28	1 2 3 19 7 9 23 12 13 14	hdmap10	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)=L\left(\left\{S\left(X\right)\right\}\right)$$
29	22 27 28	3eqtr3rd	$$⊢\phi \to L\left(\left\{S\left(X\right)\right\}\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)$$