Metamath Proof Explorer

Theorem omllaw4

Description: Orthomodular law equivalent. Remark in Holland95 p. 223. (Contributed by NM, 19-Oct-2011)

Ref Expression
Hypotheses omllaw4.b 
|- B = ( Base ` K )
omllaw4.l 
|- .<_ = ( le ` K )
omllaw4.m 
|- ./\ = ( meet ` K )
omllaw4.o 
|- ._|_ = ( oc ` K )
Assertion omllaw4 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X ) )

Proof

Step Hyp Ref Expression
1 omllaw4.b 
 |-  B = ( Base ` K )
2 omllaw4.l 
 |-  .<_ = ( le ` K )
3 omllaw4.m 
 |-  ./\ = ( meet ` K )
4 omllaw4.o 
 |-  ._|_ = ( oc ` K )
5 simp1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )
6 omlop 
 |-  ( K e. OML -> K e. OP )
7 6 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )
8 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
9 1 4 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
10 7 8 9 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
11 simp2 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
12 1 4 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
13 7 11 12 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
14 eqid 
 |-  ( join ` K ) = ( join ` K )
15 1 2 14 3 4 omllaw 
 |-  ( ( K e. OML /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` X ) e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
16 5 10 13 15 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
17 1 2 4 oplecon3b 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
18 6 17 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
19 omllat 
 |-  ( K e. OML -> K e. Lat )
20 19 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
21 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( ._|_ ` X ) e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) e. B )
22 20 13 8 21 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ Y ) e. B )
23 1 4 opoccl 
 |-  ( ( K e. OP /\ ( ( ._|_ ` X ) ./\ Y ) e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B )
24 7 22 23 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B )
25 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) e. B /\ Y e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B )
26 20 24 8 25 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B )
27 1 4 opcon3b 
 |-  ( ( K e. OP /\ ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) e. B /\ X e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) ) )
28 7 26 11 27 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) ) )
29 1 14 latjcom 
 |-  ( ( K e. Lat /\ ( ( ._|_ ` X ) ./\ Y ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) )
30 20 22 10 29 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) )
31 omlol 
 |-  ( K e. OML -> K e. OL )
32 31 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OL )
33 1 14 3 4 oldmm2 
 |-  ( ( K e. OL /\ ( ( ._|_ ` X ) ./\ Y ) e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) )
34 32 22 8 33 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ( ._|_ ` X ) ./\ Y ) ( join ` K ) ( ._|_ ` Y ) ) )
35 1 4 opococ 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
36 7 8 35 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
37 36 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) ./\ Y ) )
38 37 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ Y ) ) )
39 30 34 38 3eqtr4d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) )
40 39 eqeq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = ( ._|_ ` ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) ) <-> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
41 28 40 bitrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X <-> ( ._|_ ` X ) = ( ( ._|_ ` Y ) ( join ` K ) ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
42 16 18 41 3imtr4d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ( ._|_ ` ( ( ._|_ ` X ) ./\ Y ) ) ./\ Y ) = X ) )