Theorem hgmapvs

Description: Part 15 of Baer p. 50 line 6. Also line 15 in Holland95 p. 14. (Contributed by NM, 6-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hgmapvs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapvs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapvs.v	$$⊢V={\mathrm{Base}}_U$$
4		hgmapvs.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hgmapvs.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hgmapvs.b	$$⊢B={\mathrm{Base}}_R$$
7		hgmapvs.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hgmapvs.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hgmapvs.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hgmapvs.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
11		hgmapvs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hgmapvs.x	$$⊢\phi \to X\in V$$
13		hgmapvs.f	$$⊢\phi \to F\in B$$
14	1 2 3 4 5 6 7 8 9 10 11 13	hgmapval	$$⊢\phi \to G\left(F\right)=\left(\iota g\in B|\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)$$
15	14	eqcomd	$$⊢\phi \to \left(\iota g\in B|\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)=G\left(F\right)$$
16	1 2 5 6 10 11 13	hgmapcl	$$⊢\phi \to G\left(F\right)\in B$$
17	1 2 3 4 5 6 7 8 9 11 13	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)$$
18		oveq1	$$⊢g=G\left(F\right)\to g\underset{\dot{}}{\bullet }S\left(x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)$$
19	18	eqeq2d	$$⊢g=G\left(F\right)\to \left(S\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow S\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\right)$$
20	19	ralbidv	$$⊢g=G\left(F\right)\to \left(\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow \forall x\in VS\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\right)$$
21	20	riota2	$$⊢\left(G\left(F\right)\in B\wedge \exists !g\in B\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)\to \left(\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow \left(\iota g\in B|\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)=G\left(F\right)\right)$$
22	16 17 21	syl2anc	$$⊢\phi \to \left(\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow \left(\iota g\in B|\forall x\in VS\left(F\underset{\dot{}}{·}x\right)=g\underset{\dot{}}{\bullet }S\left(x\right)\right)=G\left(F\right)\right)$$
23	15 22	mpbird	$$⊢\phi \to \forall x\in VS\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)$$
24		oveq2	$$⊢x=X\to F\underset{\dot{}}{·}x=F\underset{\dot{}}{·}X$$
25	24	fveq2d	$$⊢x=X\to S\left(F\underset{\dot{}}{·}x\right)=S\left(F\underset{\dot{}}{·}X\right)$$
26		fveq2	$$⊢x=X\to S\left(x\right)=S\left(X\right)$$
27	26	oveq2d	$$⊢x=X\to G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(X\right)$$
28	25 27	eqeq12d	$$⊢x=X\to \left(S\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\leftrightarrow S\left(F\underset{\dot{}}{·}X\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
29	28	rspcva	$$⊢\left(X\in V\wedge \forall x\in VS\left(F\underset{\dot{}}{·}x\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(x\right)\right)\to S\left(F\underset{\dot{}}{·}X\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(X\right)$$
30	12 23 29	syl2anc	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)=G\left(F\right)\underset{\dot{}}{\bullet }S\left(X\right)$$