Theorem hdmap14lem15

Description: Part of proof of part 14 in Baer p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem12.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem12.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem12.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem12.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem12.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem12.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem12.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem12.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem12.f	$$⊢\phi \to F\in B$$
Assertion	hdmap14lem15	$$⊢\phi \to \exists !g\in B\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem12.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem12.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem12.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem12.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmap14lem12.b	$$⊢B={\mathrm{Base}}_R$$
7		hdmap14lem12.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap14lem12.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hdmap14lem12.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hdmap14lem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		hdmap14lem12.f	$$⊢\phi \to F\in B$$
12		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	hdmap14lem14	$$⊢\phi \to \exists !g\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)$$
15	1 2 5 6 7 12 13 10	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=B$$
16		reueq1	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=B\to \left(\exists !g\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow \exists !g\in B\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)$$
17	15 16	syl	$$⊢\phi \to \left(\exists !g\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow \exists !g\in B\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)$$
18	14 17	mpbid	$$⊢\phi \to \exists !g\in B\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)$$