Metamath Proof Explorer

Theorem hgmapcl

Description: Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015)

		Ref	Expression
	Hypotheses	hgmapcl.h	$⊢ H = LHyp (K)$
		hgmapcl.u	$⊢ U = DVecH (K) (W)$
		hgmapcl.r	$⊢ R = Scalar (U)$
		hgmapcl.b	$⊢ B = {Base}_{R}$
		hgmapcl.g	$⊢ G = HGMap (K) (W)$
		hgmapcl.k	$⊢ φ \to (K \in HL \land W \in H)$
		hgmapcl.f	$⊢ φ \to F \in B$
	Assertion	hgmapcl	$⊢ φ \to G (F) \in B$

Proof

Step	Hyp	Ref	Expression
1		hgmapcl.h	$⊢ H = LHyp (K)$
2		hgmapcl.u	$⊢ U = DVecH (K) (W)$
3		hgmapcl.r	$⊢ R = Scalar (U)$
4		hgmapcl.b	$⊢ B = {Base}_{R}$
5		hgmapcl.g	$⊢ G = HGMap (K) (W)$
6		hgmapcl.k	$⊢ φ \to (K \in HL \land W \in H)$
7		hgmapcl.f	$⊢ φ \to F \in B$
8		eqid	$⊢ {Base}_{U} = {Base}_{U}$
9		eqid	$⊢ \cdot_{U} = \cdot_{U}$
10		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
11		eqid	$⊢ \cdot_{LCDual (K) (W)} = \cdot_{LCDual (K) (W)}$
12		eqid	$⊢ HDMap (K) (W) = HDMap (K) (W)$
13	1 2 8 9 3 4 10 11 12 5 6 7	hgmapval	$⊢ φ \to G (F) = (ι g \in B \| \forall x \in {Base}_{U} HDMap (K) (W) (F \cdot_{U} x) = g \cdot_{LCDual (K) (W)} HDMap (K) (W) (x))$
14	1 2 8 9 3 4 10 11 12 6 7	hdmap14lem15	$⊢ φ \to \exists! g \in B \forall x \in {Base}_{U} HDMap (K) (W) (F \cdot_{U} x) = g \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)$
15		riotacl	$⊢ \exists! g \in B \forall x \in {Base}_{U} HDMap (K) (W) (F \cdot_{U} x) = g \cdot_{LCDual (K) (W)} HDMap (K) (W) (x) \to (ι g \in B \| \forall x \in {Base}_{U} HDMap (K) (W) (F \cdot_{U} x) = g \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)) \in B$
16	14 15	syl	$⊢ φ \to (ι g \in B \| \forall x \in {Base}_{U} HDMap (K) (W) (F \cdot_{U} x) = g \cdot_{LCDual (K) (W)} HDMap (K) (W) (x)) \in B$
17	13 16	eqeltrd	$⊢ φ \to G (F) \in B$