Metamath Proof Explorer

Theorem diaglbN

Description: Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaglb.g 
|- G = ( glb ` K )
diaglb.h 
|- H = ( LHyp ` K )
diaglb.i 
|- I = ( ( DIsoA ` K ) ` W )
Assertion diaglbN 
|- ( ( ( 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 diaglb.g 
 |-  G = ( glb ` K )
2 diaglb.h 
 |-  H = ( LHyp ` K )
3 diaglb.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
5 hlclat 
 |-  ( K e. HL -> K e. CLat )
6 5 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> K e. CLat )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 eqid 
 |-  ( le ` K ) = ( le ` K )
9 7 8 2 3 diadm 
 |-  ( ( K e. HL /\ W e. H ) -> dom I = { y e. ( Base ` K ) | y ( le ` K ) W } )
10 9 sseq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( S C_ dom I <-> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } ) )
11 10 biimpa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ dom I ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } )
12 11 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ { y e. ( Base ` K ) | y ( le ` K ) W } )
13 ssrab2 
 |-  { y e. ( Base ` K ) | y ( le ` K ) W } C_ ( Base ` K )
14 12 13 sstrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S C_ ( Base ` K ) )
15 7 1 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( G ` S ) e. ( Base ` K ) )
16 6 14 15 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( G ` S ) e. ( Base ` K ) )
17 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> S =/= (/) )
18 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
19 17 18 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> E. x x e. S )
20 hllat 
 |-  ( K e. HL -> K e. Lat )
21 20 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> K e. Lat )
22 16 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) e. ( Base ` K ) )
23 ssel2 
 |-  ( ( S C_ dom I /\ x e. S ) -> x e. dom I )
24 23 adantlr 
 |-  ( ( ( S C_ dom I /\ S =/= (/) ) /\ x e. S ) -> x e. dom I )
25 24 adantll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. dom I )
26 7 8 2 3 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) )
27 26 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) )
28 25 27 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) )
29 28 simpld 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. ( Base ` K ) )
30 7 2 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
31 30 ad3antlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> W e. ( Base ` K ) )
32 5 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> K e. CLat )
33 14 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> S C_ ( Base ` K ) )
34 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x e. S )
35 7 8 1 clatglble 
 |-  ( ( K e. CLat /\ S C_ ( Base ` K ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x )
36 32 33 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) x )
37 28 simprd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> x ( le ` K ) W )
38 7 8 21 22 29 31 36 37 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) ( le ` K ) W )
39 19 38 exlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( G ` S ) ( le ` K ) W )
40 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
41 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
42 7 8 2 40 41 3 diaelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. ( Base ` K ) /\ ( G ` S ) ( le ` K ) W ) ) -> ( f e. ( I ` ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) ) )
43 4 16 39 42 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( f e. ( I ` ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) ) )
44 r19.28zv 
 |-  ( S =/= (/) -> ( A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
45 44 ad2antll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
46 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) )
47 7 8 2 40 41 3 diaelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( f e. ( I ` x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
48 46 28 47 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ x e. S ) -> ( f e. ( I ` x ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
49 48 ralbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( A. x e. S f e. ( I ` x ) <-> A. x e. S ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
50 5 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> K e. CLat )
51 7 2 40 41 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) )
52 51 adantlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) )
53 14 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> S C_ ( Base ` K ) )
54 7 8 1 clatleglb 
 |-  ( ( K e. CLat /\ ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) /\ S C_ ( Base ` K ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) <-> A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) )
55 50 52 53 54 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) <-> A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) )
56 55 pm5.32da 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ A. x e. S ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) x ) ) )
57 45 49 56 3bitr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> A. x e. S f e. ( I ` x ) ) )
58 vex 
 |-  f e. _V
59 eliin 
 |-  ( f e. _V -> ( f e. |^|_ x e. S ( I ` x ) <-> A. x e. S f e. ( I ` x ) ) )
60 58 59 ax-mp 
 |-  ( f e. |^|_ x e. S ( I ` x ) <-> A. x e. S f e. ( I ` x ) )
61 57 60 bitr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( G ` S ) ) <-> f e. |^|_ x e. S ( I ` x ) ) )
62 43 61 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( f e. ( I ` ( G ` S ) ) <-> f e. |^|_ x e. S ( I ` x ) ) )
63 62 eqrdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ dom I /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )