# 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 = ( LHyp ` K )`
hdmaprn.c
`|- C = ( ( LCDual ` K ) ` W )`
hdmaprn.d
`|- D = ( Base ` C )`
hdmaprn.s
`|- S = ( ( HDMap ` K ) ` W )`
hdmaprn.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
Assertion hdmaprnN
`|- ( ph -> ran S = D )`

### Proof

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
` |-  ( ph -> ( K e. HL /\ W e. 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
` |-  ( ph -> S Fn ( Base ` ( ( DVecH ` K ) ` W ) ) )`
` |-  ( ( ph /\ s e. ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( K e. HL /\ W e. H ) )`
10 simpr
` |-  ( ( ph /\ s e. ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> s e. ( Base ` ( ( DVecH ` K ) ` W ) ) )`
11 1 6 7 2 3 4 9 10 hdmapcl
` |-  ( ( ph /\ s e. ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( S ` s ) e. D )`
12 11 ralrimiva
` |-  ( ph -> A. s e. ( Base ` ( ( DVecH ` K ) ` W ) ) ( S ` s ) e. D )`
13 fnfvrnss
` |-  ( ( S Fn ( Base ` ( ( DVecH ` K ) ` W ) ) /\ A. s e. ( Base ` ( ( DVecH ` K ) ` W ) ) ( S ` s ) e. D ) -> ran S C_ D )`
14 8 12 13 syl2anc
` |-  ( ph -> ran S C_ D )`
15 eqid
` |-  ( LSpan ` ( ( DVecH ` K ) ` W ) ) = ( LSpan ` ( ( DVecH ` K ) ` W ) )`
16 eqid
` |-  ( 0g ` C ) = ( 0g ` C )`
17 eqid
` |-  ( LSpan ` C ) = ( LSpan ` C )`
18 eqid
` |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )`
` |-  ( ( ph /\ s e. D ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ s e. D ) -> s e. D )`
` |-  ( ( ph /\ s e. D ) -> s e. ran S )`
` |-  ( ph -> ran S = D )`