Metamath Proof Explorer

Theorem mapdrvallem2

Description: Lemma for mapdrval . TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015)

Ref Expression
Hypotheses mapdrval.h 
|- H = ( LHyp ` K )
mapdrval.o 
|- O = ( ( ocH ` K ) ` W )
mapdrval.m 
|- M = ( ( mapd ` K ) ` W )
mapdrval.u 
|- U = ( ( DVecH ` K ) ` W )
mapdrval.s 
|- S = ( LSubSp ` U )
mapdrval.f 
|- F = ( LFnl ` U )
mapdrval.l 
|- L = ( LKer ` U )
mapdrval.d 
|- D = ( LDual ` U )
mapdrval.t 
|- T = ( LSubSp ` D )
mapdrval.c 
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
mapdrval.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdrval.r 
|- ( ph -> R e. T )
mapdrval.e 
|- ( ph -> R C_ C )
mapdrval.q 
|- Q = U_ h e. R ( O ` ( L ` h ) )
mapdrval.v 
|- V = ( Base ` U )
mapdrvallem2.a 
|- A = ( LSAtoms ` U )
mapdrvallem2.n 
|- N = ( LSpan ` U )
mapdrvallem2.z 
|- .0. = ( 0g ` U )
mapdrvallem2.y 
|- Y = ( 0g ` D )
Assertion mapdrvallem2 
|- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } C_ R )

Proof

Step Hyp Ref Expression
1 mapdrval.h 
 |-  H = ( LHyp ` K )
2 mapdrval.o 
 |-  O = ( ( ocH ` K ) ` W )
3 mapdrval.m 
 |-  M = ( ( mapd ` K ) ` W )
4 mapdrval.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 mapdrval.s 
 |-  S = ( LSubSp ` U )
6 mapdrval.f 
 |-  F = ( LFnl ` U )
7 mapdrval.l 
 |-  L = ( LKer ` U )
8 mapdrval.d 
 |-  D = ( LDual ` U )
9 mapdrval.t 
 |-  T = ( LSubSp ` D )
10 mapdrval.c 
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
11 mapdrval.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 mapdrval.r 
 |-  ( ph -> R e. T )
13 mapdrval.e 
 |-  ( ph -> R C_ C )
14 mapdrval.q 
 |-  Q = U_ h e. R ( O ` ( L ` h ) )
15 mapdrval.v 
 |-  V = ( Base ` U )
16 mapdrvallem2.a 
 |-  A = ( LSAtoms ` U )
17 mapdrvallem2.n 
 |-  N = ( LSpan ` U )
18 mapdrvallem2.z 
 |-  .0. = ( 0g ` U )
19 mapdrvallem2.y 
 |-  Y = ( 0g ` D )
20 eleq1 
 |-  ( f = Y -> ( f e. R <-> Y e. R ) )
21 11 3ad2ant1 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> ( K e. HL /\ W e. H ) )
22 21 adantr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> ( K e. HL /\ W e. H ) )
23 simpl2 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> f e. C )
24 simpr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> f =/= Y )
25 eldifsn 
 |-  ( f e. ( C \ { Y } ) <-> ( f e. C /\ f =/= Y ) )
26 23 24 25 sylanbrc 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> f e. ( C \ { Y } ) )
27 1 2 4 15 17 18 6 7 8 19 10 22 26 lcfl8b 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> E. x e. ( V \ { .0. } ) ( O ` ( L ` f ) ) = ( N ` { x } ) )
28 simp1l3 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( O ` ( L ` f ) ) C_ Q )
29 eqimss2 
 |-  ( ( O ` ( L ` f ) ) = ( N ` { x } ) -> ( N ` { x } ) C_ ( O ` ( L ` f ) ) )
30 29 3ad2ant3 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( N ` { x } ) C_ ( O ` ( L ` f ) ) )
31 1 4 11 dvhlmod 
 |-  ( ph -> U e. LMod )
32 31 3ad2ant1 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> U e. LMod )
33 32 adantr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> U e. LMod )
34 33 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> U e. LMod )
35 22 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( K e. HL /\ W e. H ) )
36 10 lcfl1lem 
 |-  ( f e. C <-> ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) ) )
37 36 simplbi 
 |-  ( f e. C -> f e. F )
38 37 3ad2ant2 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> f e. F )
39 38 adantr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> f e. F )
40 39 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> f e. F )
41 15 6 7 34 40 lkrssv 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( L ` f ) C_ V )
42 1 4 15 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` f ) C_ V ) -> ( O ` ( L ` f ) ) e. S )
43 35 41 42 syl2anc 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( O ` ( L ` f ) ) e. S )
44 eldifi 
 |-  ( x e. ( V \ { .0. } ) -> x e. V )
45 44 3ad2ant2 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> x e. V )
46 15 5 17 34 43 45 ellspsn5b 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( x e. ( O ` ( L ` f ) ) <-> ( N ` { x } ) C_ ( O ` ( L ` f ) ) ) )
47 30 46 mpbird 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> x e. ( O ` ( L ` f ) ) )
48 28 47 sseldd 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> x e. Q )
49 48 14 eleqtrdi 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> x e. U_ h e. R ( O ` ( L ` h ) ) )
50 eliun 
 |-  ( x e. U_ h e. R ( O ` ( L ` h ) ) <-> E. h e. R x e. ( O ` ( L ` h ) ) )
51 49 50 sylib 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> E. h e. R x e. ( O ` ( L ` h ) ) )
52 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
53 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
54 eqid 
 |-  ( .s ` D ) = ( .s ` D )
55 1 4 11 dvhlvec 
 |-  ( ph -> U e. LVec )
56 55 3ad2ant1 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> U e. LVec )
57 56 adantr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> U e. LVec )
58 57 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> U e. LVec )
59 58 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> U e. LVec )
60 simpr 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> h e. R )
61 simp1l1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ph )
62 61 adantr 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> ph )
63 62 13 syl 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> R C_ C )
64 63 sseld 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> ( h e. R -> h e. C ) )
65 10 lcfl1lem 
 |-  ( h e. C <-> ( h e. F /\ ( O ` ( O ` ( L ` h ) ) ) = ( L ` h ) ) )
66 65 simplbi 
 |-  ( h e. C -> h e. F )
67 64 66 syl6 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> ( h e. R -> h e. F ) )
68 60 67 mpd 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> h e. F )
69 68 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> h e. F )
70 40 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> f e. F )
71 simpll3 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( O ` ( L ` f ) ) = ( N ` { x } ) )
72 34 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> U e. LMod )
73 35 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( K e. HL /\ W e. H ) )
74 15 6 7 72 69 lkrssv 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( L ` h ) C_ V )
75 1 4 15 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` h ) C_ V ) -> ( O ` ( L ` h ) ) e. S )
76 73 74 75 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( O ` ( L ` h ) ) e. S )
77 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> x e. ( O ` ( L ` h ) ) )
78 5 17 72 76 77 ellspsn5 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( N ` { x } ) C_ ( O ` ( L ` h ) ) )
79 simpll2 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> x e. ( V \ { .0. } ) )
80 15 17 18 16 72 79 lsatlspsn 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( N ` { x } ) e. A )
81 1 2 4 18 16 6 7 73 69 dochsat0 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( ( O ` ( L ` h ) ) e. A \/ ( O ` ( L ` h ) ) = { .0. } ) )
82 18 16 59 80 81 lsatcmp2 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( ( N ` { x } ) C_ ( O ` ( L ` h ) ) <-> ( N ` { x } ) = ( O ` ( L ` h ) ) ) )
83 78 82 mpbid 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( N ` { x } ) = ( O ` ( L ` h ) ) )
84 71 83 eqtr2d 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( O ` ( L ` h ) ) = ( O ` ( L ` f ) ) )
85 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
86 61 13 syl 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> R C_ C )
87 86 sselda 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> h e. C )
88 87 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> h e. C )
89 1 85 2 4 6 7 10 73 69 lcfl5 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( h e. C <-> ( L ` h ) e. ran ( ( DIsoH ` K ) ` W ) ) )
90 88 89 mpbid 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( L ` h ) e. ran ( ( DIsoH ` K ) ` W ) )
91 simp1l2 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> f e. C )
92 91 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> f e. C )
93 1 85 2 4 6 7 10 73 70 lcfl5 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( f e. C <-> ( L ` f ) e. ran ( ( DIsoH ` K ) ` W ) ) )
94 92 93 mpbid 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( L ` f ) e. ran ( ( DIsoH ` K ) ` W ) )
95 1 85 2 73 90 94 doch11 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( ( O ` ( L ` h ) ) = ( O ` ( L ` f ) ) <-> ( L ` h ) = ( L ` f ) ) )
96 84 95 mpbid 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> ( L ` h ) = ( L ` f ) )
97 52 53 6 7 8 54 59 69 70 96 eqlkr4 
 |-  ( ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) /\ x e. ( O ` ( L ` h ) ) ) -> E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) )
98 97 ex 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) /\ h e. R ) -> ( x e. ( O ` ( L ` h ) ) -> E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) ) )
99 98 reximdva 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( E. h e. R x e. ( O ` ( L ` h ) ) -> E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) ) )
100 51 99 mpd 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) )
101 eleq1 
 |-  ( f = ( r ( .s ` D ) h ) -> ( f e. R <-> ( r ( .s ` D ) h ) e. R ) )
102 101 reximi 
 |-  ( E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) -> E. r e. ( Base ` ( Scalar ` U ) ) ( f e. R <-> ( r ( .s ` D ) h ) e. R ) )
103 102 reximi 
 |-  ( E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) -> E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) ( f e. R <-> ( r ( .s ` D ) h ) e. R ) )
104 rexcom 
 |-  ( E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) ( f e. R <-> ( r ( .s ` D ) h ) e. R ) <-> E. r e. ( Base ` ( Scalar ` U ) ) E. h e. R ( f e. R <-> ( r ( .s ` D ) h ) e. R ) )
105 df-rex 
 |-  ( E. h e. R ( f e. R <-> ( r ( .s ` D ) h ) e. R ) <-> E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) )
106 105 rexbii 
 |-  ( E. r e. ( Base ` ( Scalar ` U ) ) E. h e. R ( f e. R <-> ( r ( .s ` D ) h ) e. R ) <-> E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) )
107 104 106 bitri 
 |-  ( E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) ( f e. R <-> ( r ( .s ` D ) h ) e. R ) <-> E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) )
108 103 107 sylib 
 |-  ( E. h e. R E. r e. ( Base ` ( Scalar ` U ) ) f = ( r ( .s ` D ) h ) -> E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) )
109 100 108 syl 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) )
110 33 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> U e. LMod )
111 12 3ad2ant1 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> R e. T )
112 111 adantr 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> R e. T )
113 112 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> R e. T )
114 simplr 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> r e. ( Base ` ( Scalar ` U ) ) )
115 simprl 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> h e. R )
116 52 53 8 54 9 110 113 114 115 ldualssvscl 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> ( r ( .s ` D ) h ) e. R )
117 biimpr 
 |-  ( ( f e. R <-> ( r ( .s ` D ) h ) e. R ) -> ( ( r ( .s ` D ) h ) e. R -> f e. R ) )
118 117 ad2antll 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> ( ( r ( .s ` D ) h ) e. R -> f e. R ) )
119 116 118 mpd 
 |-  ( ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) /\ ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) ) -> f e. R )
120 119 ex 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) -> ( ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) -> f e. R ) )
121 120 exlimdv 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ r e. ( Base ` ( Scalar ` U ) ) ) -> ( E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) -> f e. R ) )
122 121 rexlimdva 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> ( E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) -> f e. R ) )
123 122 3ad2ant1 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> ( E. r e. ( Base ` ( Scalar ` U ) ) E. h ( h e. R /\ ( f e. R <-> ( r ( .s ` D ) h ) e. R ) ) -> f e. R ) )
124 109 123 mpd 
 |-  ( ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) /\ x e. ( V \ { .0. } ) /\ ( O ` ( L ` f ) ) = ( N ` { x } ) ) -> f e. R )
125 124 rexlimdv3a 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> ( E. x e. ( V \ { .0. } ) ( O ` ( L ` f ) ) = ( N ` { x } ) -> f e. R ) )
126 27 125 mpd 
 |-  ( ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) /\ f =/= Y ) -> f e. R )
127 8 31 lduallmod 
 |-  ( ph -> D e. LMod )
128 127 3ad2ant1 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> D e. LMod )
129 19 9 lss0cl 
 |-  ( ( D e. LMod /\ R e. T ) -> Y e. R )
130 128 111 129 syl2anc 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> Y e. R )
131 20 126 130 pm2.61ne 
 |-  ( ( ph /\ f e. C /\ ( O ` ( L ` f ) ) C_ Q ) -> f e. R )
132 131 rabssdv 
 |-  ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } C_ R )