# Metamath Proof Explorer

## Theorem 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.)

Ref Expression
Hypotheses hdmaprn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmaprn.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmaprn.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmaprn.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmaprn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hdmaprnN ${⊢}{\phi }\to \mathrm{ran}{S}={D}$

### Proof

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