Metamath Proof Explorer

Theorem dibglbN

Description: Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibglb.g 
|- G = ( glb ` K )
dibglb.h 
|- H = ( LHyp ` K )
dibglb.i 
|- I = ( ( DIsoB ` K ) ` W )
Assertion dibglbN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )

Proof

Step Hyp Ref Expression
1 dibglb.g 
 |-  G = ( glb ` K )
2 dibglb.h 
 |-  H = ( LHyp ` K )
3 dibglb.i 
 |-  I = ( ( DIsoB ` K ) ` W )
4 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
5 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ dom I )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 6 7 2 3 dibdmN 
 |-  ( ( K e. HL /\ W e. H ) -> dom I = { y e. ( Base ` K ) | y ( le ` K ) W } )
9 8 sseq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( S C_ dom I <-> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) )
10 9 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( S C_ dom I <-> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) )
11 5 10 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } )
12 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S =/= (/) )
13 2 3 dibvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` ( G ` S ) ) )
14 13 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> Rel ( I ` ( G ` S ) ) )
15 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
16 15 biimpi 
 |-  ( S =/= (/) -> E. x x e. S )
17 16 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> E. x x e. S )
18 2 3 dibvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` x ) )
19 18 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> Rel ( I ` x ) )
20 19 a1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( x e. S -> Rel ( I ` x ) ) )
21 20 ancld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( x e. S -> ( x e. S /\ Rel ( I ` x ) ) ) )
22 21 eximdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( E. x x e. S -> E. x ( x e. S /\ Rel ( I ` x ) ) ) )
23 17 22 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> E. x ( x e. S /\ Rel ( I ` x ) ) )
24 df-rex 
 |-  ( E. x e. S Rel ( I ` x ) <-> E. x ( x e. S /\ Rel ( I ` x ) ) )
25 23 24 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> E. x e. S Rel ( I ` x ) )
26 reliin 
 |-  ( E. x e. S Rel ( I ` x ) -> Rel |^|_ x e. S ( I ` x ) )
27 25 26 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> Rel |^|_ x e. S ( I ` x ) )
28 id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) )
29 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
30 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } )
31 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
32 6 7 2 31 diadm 
 |-  ( ( K e. HL /\ W e. H ) -> dom ( ( DIsoA ` K ) ` W ) = { y e. ( Base ` K ) | y ( le ` K ) W } )
33 32 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> dom ( ( DIsoA ` K ) ` W ) = { y e. ( Base ` K ) | y ( le ` K ) W } )
34 30 33 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> S C_ dom ( ( DIsoA ` K ) ` W ) )
35 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> S =/= (/) )
36 1 2 31 diaglbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom ( ( DIsoA ` K ) ` W ) /\ S =/= (/) ) ) -> ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) = |^|_ x e. S ( ( ( DIsoA ` K ) ` W ) ` x ) )
37 29 34 35 36 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) = |^|_ x e. S ( ( ( DIsoA ` K ) ` W ) ` x ) )
38 37 eleq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) <-> f e. |^|_ x e. S ( ( ( DIsoA ` K ) ` W ) ` x ) ) )
39 vex 
 |-  f e. _V
40 eliin 
 |-  ( f e. _V -> ( f e. |^|_ x e. S ( ( ( DIsoA ` K ) ` W ) ` x ) <-> A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) ) )
41 39 40 ax-mp 
 |-  ( f e. |^|_ x e. S ( ( ( DIsoA ` K ) ` W ) ` x ) <-> A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) )
42 38 41 bitrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) <-> A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) ) )
43 42 anbi1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) <-> ( A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
44 r19.27zv 
 |-  ( S =/= (/) -> ( A. x e. S ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) <-> ( A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
45 44 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( A. x e. S ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) <-> ( A. x e. S f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
46 43 45 bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) <-> A. x e. S ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
47 hlclat 
 |-  ( K e. HL -> K e. CLat )
48 47 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> K e. CLat )
49 ssrab2 
 |-  { y e. ( Base ` K ) | y ( le ` K ) W } C_ ( Base ` K )
50 30 49 sstrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> S C_ ( Base ` K ) )
51 6 1 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( G ` S ) e. ( Base ` K ) )
52 48 50 51 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( G ` S ) e. ( Base ` K ) )
53 hllat 
 |-  ( K e. HL -> K e. Lat )
54 53 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> K e. Lat )
55 47 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> K e. CLat )
56 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } )
57 56 49 sstrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> S C_ ( Base ` K ) )
58 55 57 51 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) e. ( Base ` K ) )
59 50 sselda 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> x e. ( Base ` K ) )
60 6 2 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
61 60 ad3antlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> W e. ( Base ` K ) )
62 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> x e. S )
63 6 7 1 clatglble 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x )
64 55 57 62 63 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x )
65 30 sselda 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> x e. { y e. ( Base ` K ) | y ( le ` K ) W } )
66 breq1 
 |-  ( y = x -> ( y ( le ` K ) W <-> x ( le ` K ) W ) )
67 66 elrab 
 |-  ( x e. { y e. ( Base ` K ) | y ( le ` K ) W } <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) )
68 65 67 sylib 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) )
69 68 simprd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> x ( le ` K ) W )
70 6 7 54 58 59 61 64 69 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) W )
71 17 70 exlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( G ` S ) ( le ` K ) W )
72 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
73 eqid 
 |-  ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
74 6 7 2 72 73 31 3 dibopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. ( Base ` K ) /\ ( G ` S ) ( le ` K ) W ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
75 29 52 71 74 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( G ` S ) ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
76 opex 
 |-  <. f , s >. e. _V
77 eliin 
 |-  ( <. f , s >. e. _V -> ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) )
78 76 77 ax-mp 
 |-  ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) )
79 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) )
80 6 7 2 72 73 31 3 dibopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( <. f , s >. e. ( I ` x ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
81 79 68 80 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) /\ x e. S ) -> ( <. f , s >. e. ( I ` x ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
82 81 ralbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( A. x e. S <. f , s >. e. ( I ` x ) <-> A. x e. S ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
83 78 82 syl5bb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S ( f e. ( ( ( DIsoA ` K ) ` W ) ` x ) /\ s = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
84 46 75 83 3bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) )
85 84 eqrelrdv2 
 |-  ( ( ( Rel ( I ` ( G ` S ) ) /\ Rel |^|_ x e. S ( I ` x ) ) /\ ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )
86 14 27 28 85 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ { y e. ( Base ` K ) | y ( le ` K ) W } /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )
87 4 11 12 86 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )