Metamath Proof Explorer

Theorem hdmaprnlem16N

Description: Lemma for hdmaprnN . Eliminate v . (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem15.h 
|- H = ( LHyp ` K )
hdmaprnlem15.u 
|- U = ( ( DVecH ` K ) ` W )
hdmaprnlem15.v 
|- V = ( Base ` U )
hdmaprnlem15.n 
|- N = ( LSpan ` U )
hdmaprnlem15.c 
|- C = ( ( LCDual ` K ) ` W )
hdmaprnlem15.d 
|- D = ( Base ` C )
hdmaprnlem15.q 
|- .0. = ( 0g ` C )
hdmaprnlem15.l 
|- L = ( LSpan ` C )
hdmaprnlem15.m 
|- M = ( ( mapd ` K ) ` W )
hdmaprnlem15.s 
|- S = ( ( HDMap ` K ) ` W )
hdmaprnlem15.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmaprnlem16.se 
|- ( ph -> s e. ( D \ { .0. } ) )
Assertion hdmaprnlem16N 
|- ( ph -> s e. ran S )

Proof

Step Hyp Ref Expression
1 hdmaprnlem15.h 
 |-  H = ( LHyp ` K )
2 hdmaprnlem15.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmaprnlem15.v 
 |-  V = ( Base ` U )
4 hdmaprnlem15.n 
 |-  N = ( LSpan ` U )
5 hdmaprnlem15.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmaprnlem15.d 
 |-  D = ( Base ` C )
7 hdmaprnlem15.q 
 |-  .0. = ( 0g ` C )
8 hdmaprnlem15.l 
 |-  L = ( LSpan ` C )
9 hdmaprnlem15.m 
 |-  M = ( ( mapd ` K ) ` W )
10 hdmaprnlem15.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmaprnlem15.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmaprnlem16.se 
 |-  ( ph -> s e. ( D \ { .0. } ) )
13 1 2 11 dvhlmod 
 |-  ( ph -> U e. LMod )
14 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
15 eqid 
 |-  ( LSAtoms ` C ) = ( LSAtoms ` C )
16 1 5 11 lcdlmod 
 |-  ( ph -> C e. LMod )
17 6 8 7 15 16 12 lsatlspsn 
 |-  ( ph -> ( L ` { s } ) e. ( LSAtoms ` C ) )
18 1 9 2 14 5 15 11 17 mapdcnvatN 
 |-  ( ph -> ( `' M ` ( L ` { s } ) ) e. ( LSAtoms ` U ) )
19 3 4 14 islsati 
 |-  ( ( U e. LMod /\ ( `' M ` ( L ` { s } ) ) e. ( LSAtoms ` U ) ) -> E. v e. V ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) )
20 13 18 19 syl2anc 
 |-  ( ph -> E. v e. V ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) )
21 simpr 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) )
22 21 fveq2d 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( M ` ( `' M ` ( L ` { s } ) ) ) = ( M ` ( N ` { v } ) ) )
23 11 ad2antrr 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( K e. HL /\ W e. H ) )
24 12 eldifad 
 |-  ( ph -> s e. D )
25 eqid 
 |-  ( LSubSp ` C ) = ( LSubSp ` C )
26 6 25 8 lspsncl 
 |-  ( ( C e. LMod /\ s e. D ) -> ( L ` { s } ) e. ( LSubSp ` C ) )
27 16 24 26 syl2anc 
 |-  ( ph -> ( L ` { s } ) e. ( LSubSp ` C ) )
28 1 9 5 25 11 mapdrn2 
 |-  ( ph -> ran M = ( LSubSp ` C ) )
29 27 28 eleqtrrd 
 |-  ( ph -> ( L ` { s } ) e. ran M )
30 29 ad2antrr 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( L ` { s } ) e. ran M )
31 1 9 23 30 mapdcnvid2 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( M ` ( `' M ` ( L ` { s } ) ) ) = ( L ` { s } ) )
32 22 31 eqtr3d 
 |-  ( ( ( ph /\ v e. V ) /\ ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) ) -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
33 32 ex 
 |-  ( ( ph /\ v e. V ) -> ( ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) )
34 33 reximdva 
 |-  ( ph -> ( E. v e. V ( `' M ` ( L ` { s } ) ) = ( N ` { v } ) -> E. v e. V ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) )
35 20 34 mpd 
 |-  ( ph -> E. v e. V ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
36 11 3ad2ant1 
 |-  ( ( ph /\ v e. V /\ ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) -> ( K e. HL /\ W e. H ) )
37 12 3ad2ant1 
 |-  ( ( ph /\ v e. V /\ ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) -> s e. ( D \ { .0. } ) )
38 simp2 
 |-  ( ( ph /\ v e. V /\ ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) -> v e. V )
39 simp3 
 |-  ( ( ph /\ v e. V /\ ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
40 1 2 3 4 5 6 7 8 9 10 36 37 38 39 hdmaprnlem15N 
 |-  ( ( ph /\ v e. V /\ ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) -> s e. ran S )
41 40 rexlimdv3a 
 |-  ( ph -> ( E. v e. V ( M ` ( N ` { v } ) ) = ( L ` { s } ) -> s e. ran S ) )
42 35 41 mpd 
 |-  ( ph -> s e. ran S )