This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmtbr2N

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. ( cmbr2i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtbr2.b 
|- B = ( Base ` K )
cmtbr2.j 
|- .\/ = ( join ` K )
cmtbr2.m 
|- ./\ = ( meet ` K )
cmtbr2.o 
|- ._|_ = ( oc ` K )
cmtbr2.c 
|- C = ( cm ` K )
Assertion cmtbr2N 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cmtbr2.b 
 |-  B = ( Base ` K )
2 cmtbr2.j 
 |-  .\/ = ( join ` K )
3 cmtbr2.m 
 |-  ./\ = ( meet ` K )
4 cmtbr2.o 
 |-  ._|_ = ( oc ` K )
5 cmtbr2.c 
 |-  C = ( cm ` K )
6 1 4 5 cmt4N 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( ._|_ ` X ) C ( ._|_ ` Y ) ) )
7 simp1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )
8 omlop 
 |-  ( K e. OML -> K e. OP )
9 8 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )
10 simp2 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
11 1 4 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
12 9 10 11 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
13 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
14 1 4 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
15 9 13 14 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
16 1 2 3 4 5 cmtvalN 
 |-  ( ( K e. OML /\ ( ._|_ ` X ) e. B /\ ( ._|_ ` Y ) e. B ) -> ( ( ._|_ ` X ) C ( ._|_ ` Y ) <-> ( ._|_ ` X ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
17 7 12 15 16 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) C ( ._|_ ` Y ) <-> ( ._|_ ` X ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
18 eqcom 
 |-  ( X = ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) <-> ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) = X )
19 18 a1i 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X = ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) <-> ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) = X ) )
20 omllat 
 |-  ( K e. OML -> K e. Lat )
21 20 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
22 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
23 20 22 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
24 1 2 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X .\/ ( ._|_ ` Y ) ) e. B )
25 21 10 15 24 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ ( ._|_ ` Y ) ) e. B )
26 1 3 latmcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ ( X .\/ ( ._|_ ` Y ) ) e. B ) -> ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) e. B )
27 21 23 25 26 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) e. B )
28 1 4 opcon3b 
 |-  ( ( K e. OP /\ ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) e. B /\ X e. B ) -> ( ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) ) )
29 9 27 10 28 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) = X <-> ( ._|_ ` X ) = ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) ) )
30 omlol 
 |-  ( K e. OML -> K e. OL )
31 30 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OL )
32 1 2 3 4 oldmm1 
 |-  ( ( K e. OL /\ ( X .\/ Y ) e. B /\ ( X .\/ ( ._|_ ` Y ) ) e. B ) -> ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X .\/ Y ) ) .\/ ( ._|_ ` ( X .\/ ( ._|_ ` Y ) ) ) ) )
33 31 23 25 32 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` ( X .\/ Y ) ) .\/ ( ._|_ ` ( X .\/ ( ._|_ ` Y ) ) ) ) )
34 1 2 3 4 oldmj1 
 |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X .\/ Y ) ) = ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) )
35 30 34 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X .\/ Y ) ) = ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) )
36 1 2 3 4 oldmj1 
 |-  ( ( K e. OL /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( ._|_ ` ( X .\/ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) )
37 31 10 15 36 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( X .\/ ( ._|_ ` Y ) ) ) = ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) )
38 35 37 oveq12d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( X .\/ Y ) ) .\/ ( ._|_ ` ( X .\/ ( ._|_ ` Y ) ) ) ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) )
39 33 38 eqtrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) )
40 39 eqeq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = ( ._|_ ` ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) <-> ( ._|_ ` X ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
41 19 29 40 3bitrrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` X ) = ( ( ( ._|_ ` X ) ./\ ( ._|_ ` Y ) ) .\/ ( ( ._|_ ` X ) ./\ ( ._|_ ` ( ._|_ ` Y ) ) ) ) <-> X = ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) )
42 6 17 41 3bitrd 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X .\/ Y ) ./\ ( X .\/ ( ._|_ ` Y ) ) ) ) )