Metamath Proof Explorer

Theorem dihmeetlem2N

Description: Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem2.b 
|- B = ( Base ` K )
dihmeetlem2.m 
|- ./\ = ( meet ` K )
dihmeetlem2.h 
|- H = ( LHyp ` K )
dihmeetlem2.i 
|- I = ( ( DIsoH ` K ) ` W )
dihmeetlem2.l 
|- .<_ = ( le ` K )
dihmeetlem2.j 
|- .\/ = ( join ` K )
dihmeetlem2.a 
|- A = ( Atoms ` K )
dihmeetlem2.p 
|- P = ( ( oc ` K ) ` W )
dihmeetlem2.t 
|- T = ( ( LTrn ` K ) ` W )
dihmeetlem2.r 
|- R = ( ( trL ` K ) ` W )
dihmeetlem2.e 
|- E = ( ( TEndo ` K ) ` W )
dihmeetlem2.g 
|- G = ( iota_ h e. T ( h ` P ) = q )
dihmeetlem2.o 
|- .0. = ( h e. T |-> ( _I |` B ) )
Assertion dihmeetlem2N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) )

Proof

Step Hyp Ref Expression
1 dihmeetlem2.b 
 |-  B = ( Base ` K )
2 dihmeetlem2.m 
 |-  ./\ = ( meet ` K )
3 dihmeetlem2.h 
 |-  H = ( LHyp ` K )
4 dihmeetlem2.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihmeetlem2.l 
 |-  .<_ = ( le ` K )
6 dihmeetlem2.j 
 |-  .\/ = ( join ` K )
7 dihmeetlem2.a 
 |-  A = ( Atoms ` K )
8 dihmeetlem2.p 
 |-  P = ( ( oc ` K ) ` W )
9 dihmeetlem2.t 
 |-  T = ( ( LTrn ` K ) ` W )
10 dihmeetlem2.r 
 |-  R = ( ( trL ` K ) ` W )
11 dihmeetlem2.e 
 |-  E = ( ( TEndo ` K ) ` W )
12 dihmeetlem2.g 
 |-  G = ( iota_ h e. T ( h ` P ) = q )
13 dihmeetlem2.o 
 |-  .0. = ( h e. T |-> ( _I |` B ) )
14 eqid 
 |-  ( glb ` K ) = ( glb ` K )
15 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> K e. HL )
16 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> X e. B )
17 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> Y e. B )
18 14 2 15 16 17 meetval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) = ( ( glb ` K ) ` { X , Y } ) )
19 18 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ Y ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( ( glb ` K ) ` { X , Y } ) ) )
20 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
21 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
22 1 5 3 21 dibeldmN 
 |-  ( ( K e. HL /\ W e. H ) -> ( X e. dom ( ( DIsoB ` K ) ` W ) <-> ( X e. B /\ X .<_ W ) ) )
23 22 biimpar 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> X e. dom ( ( DIsoB ` K ) ` W ) )
24 23 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> X e. dom ( ( DIsoB ` K ) ` W ) )
25 1 5 3 21 dibeldmN 
 |-  ( ( K e. HL /\ W e. H ) -> ( Y e. dom ( ( DIsoB ` K ) ` W ) <-> ( Y e. B /\ Y .<_ W ) ) )
26 25 biimpar 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> Y e. dom ( ( DIsoB ` K ) ` W ) )
27 26 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> Y e. dom ( ( DIsoB ` K ) ` W ) )
28 prssg 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( X e. dom ( ( DIsoB ` K ) ` W ) /\ Y e. dom ( ( DIsoB ` K ) ` W ) ) <-> { X , Y } C_ dom ( ( DIsoB ` K ) ` W ) ) )
29 16 17 28 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( X e. dom ( ( DIsoB ` K ) ` W ) /\ Y e. dom ( ( DIsoB ` K ) ` W ) ) <-> { X , Y } C_ dom ( ( DIsoB ` K ) ` W ) ) )
30 24 27 29 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> { X , Y } C_ dom ( ( DIsoB ` K ) ` W ) )
31 prnzg 
 |-  ( X e. B -> { X , Y } =/= (/) )
32 16 31 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> { X , Y } =/= (/) )
33 14 3 21 dibglbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( { X , Y } C_ dom ( ( DIsoB ` K ) ` W ) /\ { X , Y } =/= (/) ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( glb ` K ) ` { X , Y } ) ) = |^|_ x e. { X , Y } ( ( ( DIsoB ` K ) ` W ) ` x ) )
34 20 30 32 33 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( ( glb ` K ) ` { X , Y } ) ) = |^|_ x e. { X , Y } ( ( ( DIsoB ` K ) ` W ) ` x ) )
35 19 34 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ Y ) ) = |^|_ x e. { X , Y } ( ( ( DIsoB ` K ) ` W ) ` x ) )
36 15 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> K e. Lat )
37 1 2 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
38 36 16 17 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) e. B )
39 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> W e. H )
40 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
41 39 40 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> W e. B )
42 1 5 2 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
43 36 16 17 42 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) .<_ X )
44 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> X .<_ W )
45 1 5 36 38 16 41 43 44 lattrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) .<_ W )
46 1 5 3 4 21 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ Y ) e. B /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ Y ) ) )
47 20 38 45 46 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ Y ) ) )
48 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x e. { X , Y } ) -> ( K e. HL /\ W e. H ) )
49 vex 
 |-  x e. _V
50 49 elpr 
 |-  ( x e. { X , Y } <-> ( x = X \/ x = Y ) )
51 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = X ) -> ( X e. B /\ X .<_ W ) )
52 eleq1 
 |-  ( x = X -> ( x e. B <-> X e. B ) )
53 breq1 
 |-  ( x = X -> ( x .<_ W <-> X .<_ W ) )
54 52 53 anbi12d 
 |-  ( x = X -> ( ( x e. B /\ x .<_ W ) <-> ( X e. B /\ X .<_ W ) ) )
55 54 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = X ) -> ( ( x e. B /\ x .<_ W ) <-> ( X e. B /\ X .<_ W ) ) )
56 51 55 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = X ) -> ( x e. B /\ x .<_ W ) )
57 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = Y ) -> ( Y e. B /\ Y .<_ W ) )
58 eleq1 
 |-  ( x = Y -> ( x e. B <-> Y e. B ) )
59 breq1 
 |-  ( x = Y -> ( x .<_ W <-> Y .<_ W ) )
60 58 59 anbi12d 
 |-  ( x = Y -> ( ( x e. B /\ x .<_ W ) <-> ( Y e. B /\ Y .<_ W ) ) )
61 60 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = Y ) -> ( ( x e. B /\ x .<_ W ) <-> ( Y e. B /\ Y .<_ W ) ) )
62 57 61 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x = Y ) -> ( x e. B /\ x .<_ W ) )
63 56 62 jaodan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( x = X \/ x = Y ) ) -> ( x e. B /\ x .<_ W ) )
64 50 63 sylan2b 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x e. { X , Y } ) -> ( x e. B /\ x .<_ W ) )
65 1 5 3 4 21 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. B /\ x .<_ W ) ) -> ( I ` x ) = ( ( ( DIsoB ` K ) ` W ) ` x ) )
66 48 64 65 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ x e. { X , Y } ) -> ( I ` x ) = ( ( ( DIsoB ` K ) ` W ) ` x ) )
67 66 iineq2dv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> |^|_ x e. { X , Y } ( I ` x ) = |^|_ x e. { X , Y } ( ( ( DIsoB ` K ) ` W ) ` x ) )
68 35 47 67 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = |^|_ x e. { X , Y } ( I ` x ) )
69 fveq2 
 |-  ( x = X -> ( I ` x ) = ( I ` X ) )
70 fveq2 
 |-  ( x = Y -> ( I ` x ) = ( I ` Y ) )
71 69 70 iinxprg 
 |-  ( ( X e. B /\ Y e. B ) -> |^|_ x e. { X , Y } ( I ` x ) = ( ( I ` X ) i^i ( I ` Y ) ) )
72 16 17 71 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> |^|_ x e. { X , Y } ( I ` x ) = ( ( I ` X ) i^i ( I ` Y ) ) )
73 68 72 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) )