Theorem hdmap14lem4

Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a into this one. (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	hdmap14lem4	$$⊢\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		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	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)$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmap14lem4a	$$⊢\phi \to \left(\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)\leftrightarrow \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
21	19 20	mpbid	$$⊢\phi \to \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$