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 ) )