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 ) ) )
9 5 adantr 
 |-  ( ( 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 )
19 5 adantr 
 |-  ( ( ph /\ s e. D ) -> ( K e. HL /\ W e. H ) )
20 simpr 
 |-  ( ( ph /\ s e. D ) -> s e. D )
21 1 6 7 15 2 3 16 17 18 4 19 20 hdmaprnlem17N 
 |-  ( ( ph /\ s e. D ) -> s e. ran S )
22 14 21 eqelssd 
 |-  ( ph -> ran S = D )