Metamath Proof Explorer

Theorem dih1dimatlem

Description: Lemma for dih1dimat . (Contributed by NM, 10-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h 
|- H = ( LHyp ` K )
dih1dimat.u 
|- U = ( ( DVecH ` K ) ` W )
dih1dimat.i 
|- I = ( ( DIsoH ` K ) ` W )
dih1dimat.a 
|- A = ( LSAtoms ` U )
dih1dimat.b 
|- B = ( Base ` K )
dih1dimat.l 
|- .<_ = ( le ` K )
dih1dimat.c 
|- C = ( Atoms ` K )
dih1dimat.p 
|- P = ( ( oc ` K ) ` W )
dih1dimat.t 
|- T = ( ( LTrn ` K ) ` W )
dih1dimat.r 
|- R = ( ( trL ` K ) ` W )
dih1dimat.e 
|- E = ( ( TEndo ` K ) ` W )
dih1dimat.o 
|- O = ( h e. T |-> ( _I |` B ) )
dih1dimat.d 
|- F = ( Scalar ` U )
dih1dimat.j 
|- J = ( invr ` F )
dih1dimat.v 
|- V = ( Base ` U )
dih1dimat.m 
|- .x. = ( .s ` U )
dih1dimat.s 
|- S = ( LSubSp ` U )
dih1dimat.n 
|- N = ( LSpan ` U )
dih1dimat.z 
|- .0. = ( 0g ` U )
dih1dimat.g 
|- G = ( iota_ h e. T ( h ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
Assertion dih1dimatlem 
|- ( ( ( K e. HL /\ W e. H ) /\ D e. A ) -> D e. ran I )

Proof

Step Hyp Ref Expression
1 dih1dimat.h 
 |-  H = ( LHyp ` K )
2 dih1dimat.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dih1dimat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dih1dimat.a 
 |-  A = ( LSAtoms ` U )
5 dih1dimat.b 
 |-  B = ( Base ` K )
6 dih1dimat.l 
 |-  .<_ = ( le ` K )
7 dih1dimat.c 
 |-  C = ( Atoms ` K )
8 dih1dimat.p 
 |-  P = ( ( oc ` K ) ` W )
9 dih1dimat.t 
 |-  T = ( ( LTrn ` K ) ` W )
10 dih1dimat.r 
 |-  R = ( ( trL ` K ) ` W )
11 dih1dimat.e 
 |-  E = ( ( TEndo ` K ) ` W )
12 dih1dimat.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
13 dih1dimat.d 
 |-  F = ( Scalar ` U )
14 dih1dimat.j 
 |-  J = ( invr ` F )
15 dih1dimat.v 
 |-  V = ( Base ` U )
16 dih1dimat.m 
 |-  .x. = ( .s ` U )
17 dih1dimat.s 
 |-  S = ( LSubSp ` U )
18 dih1dimat.n 
 |-  N = ( LSpan ` U )
19 dih1dimat.z 
 |-  .0. = ( 0g ` U )
20 dih1dimat.g 
 |-  G = ( iota_ h e. T ( h ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
21 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
22 1 2 21 dvhlvec 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )
23 15 18 19 4 islsat 
 |-  ( U e. LVec -> ( D e. A <-> E. v e. ( V \ { .0. } ) D = ( N ` { v } ) ) )
24 22 23 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( D e. A <-> E. v e. ( V \ { .0. } ) D = ( N ` { v } ) ) )
25 24 biimpa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ D e. A ) -> E. v e. ( V \ { .0. } ) D = ( N ` { v } ) )
26 eldifi 
 |-  ( v e. ( V \ { .0. } ) -> v e. V )
27 1 9 11 2 15 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> V = ( T X. E ) )
28 27 eleq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( v e. V <-> v e. ( T X. E ) ) )
29 26 28 syl5ib 
 |-  ( ( K e. HL /\ W e. H ) -> ( v e. ( V \ { .0. } ) -> v e. ( T X. E ) ) )
30 29 imp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( V \ { .0. } ) ) -> v e. ( T X. E ) )
31 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> s = O )
32 31 opeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> <. f , s >. = <. f , O >. )
33 32 sneqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> { <. f , s >. } = { <. f , O >. } )
34 33 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> ( N ` { <. f , s >. } ) = ( N ` { <. f , O >. } ) )
35 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( K e. HL /\ W e. H ) )
36 5 1 9 10 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) e. B )
37 6 1 9 10 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) .<_ W )
38 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
39 5 6 1 3 38 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` f ) e. B /\ ( R ` f ) .<_ W ) ) -> ( I ` ( R ` f ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` f ) ) )
40 35 36 37 39 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( I ` ( R ` f ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` f ) ) )
41 5 1 9 10 12 2 38 18 dib1dim2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( DIsoB ` K ) ` W ) ` ( R ` f ) ) = ( N ` { <. f , O >. } ) )
42 40 41 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( N ` { <. f , O >. } ) = ( I ` ( R ` f ) ) )
43 5 1 3 2 17 dihf11 
 |-  ( ( K e. HL /\ W e. H ) -> I : B -1-1-> S )
44 43 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> I : B -1-1-> S )
45 f1fn 
 |-  ( I : B -1-1-> S -> I Fn B )
46 44 45 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> I Fn B )
47 fnfvelrn 
 |-  ( ( I Fn B /\ ( R ` f ) e. B ) -> ( I ` ( R ` f ) ) e. ran I )
48 46 36 47 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( I ` ( R ` f ) ) e. ran I )
49 42 48 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( N ` { <. f , O >. } ) e. ran I )
50 49 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) -> ( N ` { <. f , O >. } ) e. ran I )
51 50 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> ( N ` { <. f , O >. } ) e. ran I )
52 34 51 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s = O ) -> ( N ` { <. f , s >. } ) e. ran I )
53 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( K e. HL /\ W e. H ) )
54 eqid 
 |-  ( Base ` F ) = ( Base ` F )
55 1 11 2 13 54 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` F ) = E )
56 53 55 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( Base ` F ) = E )
57 56 rexeqdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) <-> E. t e. E u = ( t .x. <. f , s >. ) ) )
58 simplll 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> ( K e. HL /\ W e. H ) )
59 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> t e. E )
60 opelxpi 
 |-  ( ( f e. T /\ s e. E ) -> <. f , s >. e. ( T X. E ) )
61 60 ad3antlr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> <. f , s >. e. ( T X. E ) )
62 1 9 11 2 16 dvhvscacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ <. f , s >. e. ( T X. E ) ) ) -> ( t .x. <. f , s >. ) e. ( T X. E ) )
63 58 59 61 62 syl12anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> ( t .x. <. f , s >. ) e. ( T X. E ) )
64 eleq1a 
 |-  ( ( t .x. <. f , s >. ) e. ( T X. E ) -> ( u = ( t .x. <. f , s >. ) -> u e. ( T X. E ) ) )
65 63 64 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> ( u = ( t .x. <. f , s >. ) -> u e. ( T X. E ) ) )
66 65 rexlimdva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( E. t e. E u = ( t .x. <. f , s >. ) -> u e. ( T X. E ) ) )
67 66 pm4.71rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( E. t e. E u = ( t .x. <. f , s >. ) <-> ( u e. ( T X. E ) /\ E. t e. E u = ( t .x. <. f , s >. ) ) ) )
68 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> f e. T )
69 68 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> f e. T )
70 simplrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> s e. E )
71 70 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> s e. E )
72 1 9 11 2 16 dvhopvsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ f e. T /\ s e. E ) ) -> ( t .x. <. f , s >. ) = <. ( t ` f ) , ( t o. s ) >. )
73 58 59 69 71 72 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> ( t .x. <. f , s >. ) = <. ( t ` f ) , ( t o. s ) >. )
74 73 eqeq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) /\ t e. E ) -> ( u = ( t .x. <. f , s >. ) <-> u = <. ( t ` f ) , ( t o. s ) >. ) )
75 74 rexbidva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( E. t e. E u = ( t .x. <. f , s >. ) <-> E. t e. E u = <. ( t ` f ) , ( t o. s ) >. ) )
76 75 anbi2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( u e. ( T X. E ) /\ E. t e. E u = ( t .x. <. f , s >. ) ) <-> ( u e. ( T X. E ) /\ E. t e. E u = <. ( t ` f ) , ( t o. s ) >. ) ) )
77 57 67 76 3bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) <-> ( u e. ( T X. E ) /\ E. t e. E u = <. ( t ` f ) , ( t o. s ) >. ) ) )
78 77 abbidv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> { u | E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) } = { u | ( u e. ( T X. E ) /\ E. t e. E u = <. ( t ` f ) , ( t o. s ) >. ) } )
79 df-rab 
 |-  { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } = { u | ( u e. ( T X. E ) /\ E. t e. E u = <. ( t ` f ) , ( t o. s ) >. ) }
80 78 79 eqtr4di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> { u | E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) } = { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } )
81 ssrab2 
 |-  { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } C_ ( T X. E )
82 relxp 
 |-  Rel ( T X. E )
83 relss 
 |-  ( { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } C_ ( T X. E ) -> ( Rel ( T X. E ) -> Rel { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } ) )
84 81 82 83 mp2 
 |-  Rel { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. }
85 relopabv 
 |-  Rel { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) }
86 vex 
 |-  i e. _V
87 vex 
 |-  p e. _V
88 eqeq1 
 |-  ( g = i -> ( g = ( r ` G ) <-> i = ( r ` G ) ) )
89 88 anbi1d 
 |-  ( g = i -> ( ( g = ( r ` G ) /\ r e. E ) <-> ( i = ( r ` G ) /\ r e. E ) ) )
90 fveq1 
 |-  ( r = p -> ( r ` G ) = ( p ` G ) )
91 90 eqeq2d 
 |-  ( r = p -> ( i = ( r ` G ) <-> i = ( p ` G ) ) )
92 eleq1w 
 |-  ( r = p -> ( r e. E <-> p e. E ) )
93 91 92 anbi12d 
 |-  ( r = p -> ( ( i = ( r ` G ) /\ r e. E ) <-> ( i = ( p ` G ) /\ p e. E ) ) )
94 86 87 89 93 opelopab 
 |-  ( <. i , p >. e. { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } <-> ( i = ( p ` G ) /\ p e. E ) )
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) )
96 95 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) )
97 opelxp 
 |-  ( <. i , p >. e. ( T X. E ) <-> ( i e. T /\ p e. E ) )
98 86 87 opth 
 |-  ( <. i , p >. = <. ( t ` f ) , ( t o. s ) >. <-> ( i = ( t ` f ) /\ p = ( t o. s ) ) )
99 98 rexbii 
 |-  ( E. t e. E <. i , p >. = <. ( t ` f ) , ( t o. s ) >. <-> E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) )
100 97 99 anbi12i 
 |-  ( ( <. i , p >. e. ( T X. E ) /\ E. t e. E <. i , p >. = <. ( t ` f ) , ( t o. s ) >. ) <-> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) )
101 96 100 bitr4di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> ( <. i , p >. e. ( T X. E ) /\ E. t e. E <. i , p >. = <. ( t ` f ) , ( t o. s ) >. ) ) )
102 eqeq1 
 |-  ( u = <. i , p >. -> ( u = <. ( t ` f ) , ( t o. s ) >. <-> <. i , p >. = <. ( t ` f ) , ( t o. s ) >. ) )
103 102 rexbidv 
 |-  ( u = <. i , p >. -> ( E. t e. E u = <. ( t ` f ) , ( t o. s ) >. <-> E. t e. E <. i , p >. = <. ( t ` f ) , ( t o. s ) >. ) )
104 103 elrab 
 |-  ( <. i , p >. e. { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } <-> ( <. i , p >. e. ( T X. E ) /\ E. t e. E <. i , p >. = <. ( t ` f ) , ( t o. s ) >. ) )
105 101 104 bitr4di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> <. i , p >. e. { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } ) )
106 94 105 bitr2id 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( <. i , p >. e. { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } <-> <. i , p >. e. { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } ) )
107 84 85 106 eqrelrdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> { u e. ( T X. E ) | E. t e. E u = <. ( t ` f ) , ( t o. s ) >. } = { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } )
108 80 107 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> { u | E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) } = { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } )
109 1 2 53 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> U e. LMod )
110 1 9 11 2 15 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) -> <. f , s >. e. V )
111 110 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> <. f , s >. e. V )
112 13 54 15 16 18 lspsn 
 |-  ( ( U e. LMod /\ <. f , s >. e. V ) -> ( N ` { <. f , s >. } ) = { u | E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) } )
113 109 111 112 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( N ` { <. f , s >. } ) = { u | E. t e. ( Base ` F ) u = ( t .x. <. f , s >. ) } )
114 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> s =/= O )
115 5 1 9 11 12 2 13 14 tendoinvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( ( J ` s ) e. E /\ ( J ` s ) =/= O ) )
116 115 simpld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( J ` s ) e. E )
117 53 70 114 116 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( J ` s ) e. E )
118 1 9 11 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( J ` s ) e. E /\ f e. T ) -> ( ( J ` s ) ` f ) e. T )
119 53 117 68 118 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( J ` s ) ` f ) e. T )
120 6 7 1 8 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. C /\ -. P .<_ W ) )
121 53 120 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( P e. C /\ -. P .<_ W ) )
122 6 7 1 9 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( J ` s ) ` f ) e. T /\ ( P e. C /\ -. P .<_ W ) ) -> ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) )
123 53 119 121 122 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) )
124 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
125 6 7 1 124 3 dihvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) ) -> ( I ` ( ( ( J ` s ) ` f ) ` P ) ) = ( ( ( DIsoC ` K ) ` W ) ` ( ( ( J ` s ) ` f ) ` P ) ) )
126 53 123 125 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( I ` ( ( ( J ` s ) ` f ) ` P ) ) = ( ( ( DIsoC ` K ) ` W ) ` ( ( ( J ` s ) ` f ) ` P ) ) )
127 6 7 1 8 9 11 124 20 dicval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) ) -> ( ( ( DIsoC ` K ) ` W ) ` ( ( ( J ` s ) ` f ) ` P ) ) = { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } )
128 53 123 127 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( ( DIsoC ` K ) ` W ) ` ( ( ( J ` s ) ` f ) ` P ) ) = { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } )
129 126 128 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( I ` ( ( ( J ` s ) ` f ) ` P ) ) = { <. g , r >. | ( g = ( r ` G ) /\ r e. E ) } )
130 108 113 129 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( N ` { <. f , s >. } ) = ( I ` ( ( ( J ` s ) ` f ) ` P ) ) )
131 5 1 3 dihfn 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn B )
132 131 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) -> I Fn B )
133 132 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> I Fn B )
134 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> K e. HL )
135 hlop 
 |-  ( K e. HL -> K e. OP )
136 134 135 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> K e. OP )
137 5 1 lhpbase 
 |-  ( W e. H -> W e. B )
138 137 ad3antlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> W e. B )
139 eqid 
 |-  ( oc ` K ) = ( oc ` K )
140 5 139 opoccl 
 |-  ( ( K e. OP /\ W e. B ) -> ( ( oc ` K ) ` W ) e. B )
141 136 138 140 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( oc ` K ) ` W ) e. B )
142 8 141 eqeltrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> P e. B )
143 5 1 9 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( J ` s ) ` f ) e. T /\ P e. B ) -> ( ( ( J ` s ) ` f ) ` P ) e. B )
144 53 119 142 143 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( ( ( J ` s ) ` f ) ` P ) e. B )
145 fnfvelrn 
 |-  ( ( I Fn B /\ ( ( ( J ` s ) ` f ) ` P ) e. B ) -> ( I ` ( ( ( J ` s ) ` f ) ` P ) ) e. ran I )
146 133 144 145 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( I ` ( ( ( J ` s ) ` f ) ` P ) ) e. ran I )
147 130 146 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) /\ s =/= O ) -> ( N ` { <. f , s >. } ) e. ran I )
148 52 147 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) ) -> ( N ` { <. f , s >. } ) e. ran I )
149 148 ralrimivva 
 |-  ( ( K e. HL /\ W e. H ) -> A. f e. T A. s e. E ( N ` { <. f , s >. } ) e. ran I )
150 sneq 
 |-  ( v = <. f , s >. -> { v } = { <. f , s >. } )
151 150 fveq2d 
 |-  ( v = <. f , s >. -> ( N ` { v } ) = ( N ` { <. f , s >. } ) )
152 151 eleq1d 
 |-  ( v = <. f , s >. -> ( ( N ` { v } ) e. ran I <-> ( N ` { <. f , s >. } ) e. ran I ) )
153 152 ralxp 
 |-  ( A. v e. ( T X. E ) ( N ` { v } ) e. ran I <-> A. f e. T A. s e. E ( N ` { <. f , s >. } ) e. ran I )
154 149 153 sylibr 
 |-  ( ( K e. HL /\ W e. H ) -> A. v e. ( T X. E ) ( N ` { v } ) e. ran I )
155 154 r19.21bi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( T X. E ) ) -> ( N ` { v } ) e. ran I )
156 30 155 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( V \ { .0. } ) ) -> ( N ` { v } ) e. ran I )
157 eleq1a 
 |-  ( ( N ` { v } ) e. ran I -> ( D = ( N ` { v } ) -> D e. ran I ) )
158 156 157 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( V \ { .0. } ) ) -> ( D = ( N ` { v } ) -> D e. ran I ) )
159 158 rexlimdva 
 |-  ( ( K e. HL /\ W e. H ) -> ( E. v e. ( V \ { .0. } ) D = ( N ` { v } ) -> D e. ran I ) )
160 159 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ D e. A ) -> ( E. v e. ( V \ { .0. } ) D = ( N ` { v } ) -> D e. ran I ) )
161 25 160 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ D e. A ) -> D e. ran I )