hdmaprnN

Description: Part of proof of part 12 in Baer p. 49 line 21, As=B. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		hdmaprn.h	$⊢ H = LHyp (K)$
2		hdmaprn.c	$⊢ C = LCDual (K) (W)$
3		hdmaprn.d	$⊢ D = {Base}_{C}$
4		hdmaprn.s	$⊢ S = HDMap (K) (W)$
5		hdmaprn.k	$⊢ φ \to (K \in HL \land W \in H)$
6		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
7		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
8	1 6 7 4 5	hdmapfnN	$⊢ φ \to S Fn {Base}_{DVecH (K) (W)}$
9	5	adantr	$⊢ (φ \land s \in {Base}_{DVecH (K) (W)}) \to (K \in HL \land W \in H)$
10		simpr	$⊢ (φ \land s \in {Base}_{DVecH (K) (W)}) \to s \in {Base}_{DVecH (K) (W)}$
11	1 6 7 2 3 4 9 10	hdmapcl	$⊢ (φ \land s \in {Base}_{DVecH (K) (W)}) \to S (s) \in D$
12	11	ralrimiva	$⊢ φ \to \forall s \in {Base}_{DVecH (K) (W)} S (s) \in D$
13		fnfvrnss	$⊢ (S Fn {Base}_{DVecH (K) (W)} \land \forall s \in {Base}_{DVecH (K) (W)} S (s) \in D) \to ran S \subseteq D$
14	8 12 13	syl2anc	$⊢ φ \to ran S \subseteq D$
15		eqid	$⊢ LSpan (DVecH (K) (W)) = LSpan (DVecH (K) (W))$
16		eqid	$⊢ 0_{C} = 0_{C}$
17		eqid	$⊢ LSpan (C) = LSpan (C)$
18		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
19	5	adantr	$⊢ (φ \land s \in D) \to (K \in HL \land W \in H)$
20		simpr	$⊢ (φ \land s \in D) \to s \in D$
21	1 6 7 15 2 3 16 17 18 4 19 20	hdmaprnlem17N	$⊢ (φ \land s \in D) \to s \in ran S$
22	14 21	eqelssd	$⊢ φ \to ran S = D$

Metamath Proof Explorer