Theorem hdmap14lem1

Description: Prior to part 14 in Baer p. 49, line 25. (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	hdmap14lem1	$$⊢\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		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	17	eldifad	$$⊢\phi \to X\in V$$
20	18	eldifad	$$⊢\phi \to F\in B$$
21		eldifsni	$$⊢F\in \left(B\setminus \left\{Z\right\}\right)\to F\ne Z$$
22	18 21	syl	$$⊢\phi \to F\ne Z$$
23	1 2 3 4 6 7 9 10 11 12 13 15 16 19 20 8 22	hdmap14lem1a	$$⊢\phi \to L\left(\left\{S\left(X\right)\right\}\right)=L\left(\left\{S\left(F\underset{\dot{}}{·}X\right)\right\}\right)$$