Theorem hdmap14lem7

Description: Combine cases of F . TODO: Can this be done at once in hdmap14lem3 , in order to get rid of hdmap14lem6 ? Perhaps modify lspsneu to become E! k e. K instead of E! k e. ( K \ { .0. } ) ? (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem7.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem7.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem7.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap14lem7.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem7.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem7.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem7.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem7.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hdmap14lem7.a	$$⊢A={\mathrm{Base}}_P$$
	hdmap14lem7.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem7.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap14lem7.f	$$⊢\phi \to F\in B$$
Assertion	hdmap14lem7	$$⊢\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		hdmap14lem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem7.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem7.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem7.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap14lem7.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmap14lem7.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmap14lem7.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		hdmap14lem7.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
10		hdmap14lem7.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
11		hdmap14lem7.a	$$⊢A={\mathrm{Base}}_P$$
12		hdmap14lem7.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
13		hdmap14lem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		hdmap14lem7.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15		hdmap14lem7.f	$$⊢\phi \to F\in B$$
16		eqid	$$⊢0_R=0_R$$
17		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
18		eqid	$$⊢0_P=0_P$$
19	13	adantr	$$⊢\left(\phi \wedge F=0_R\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
20	14	adantr	$$⊢\left(\phi \wedge F=0_R\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
21		simpr	$$⊢\left(\phi \wedge F=0_R\right)\to F=0_R$$
22	1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 19 20 21	hdmap14lem6	$$⊢\left(\phi \wedge F=0_R\right)\to \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
23	13	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
24	14	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25	15	adantr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to F\in B$$
26		simpr	$$⊢\left(\phi \wedge F\ne 0_R\right)\to F\ne 0_R$$
27		eldifsn	$$⊢F\in \left(B\setminus \left\{0_R\right\}\right)\leftrightarrow \left(F\in B\wedge F\ne 0_R\right)$$
28	25 26 27	sylanbrc	$$⊢\left(\phi \wedge F\ne 0_R\right)\to F\in \left(B\setminus \left\{0_R\right\}\right)$$
29	1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 23 24 28	hdmap14lem4	$$⊢\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)$$
30	22 29	pm2.61dane	$$⊢\phi \to \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$