Metamath Proof Explorer

Theorem cmt2N

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. ( cmcm2i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmt2.b 
|- B = ( Base ` K )
cmt2.o 
|- ._|_ = ( oc ` K )
cmt2.c 
|- C = ( cm ` K )
Assertion cmt2N 
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X C ( ._|_ ` Y ) ) )

Proof

Step Hyp Ref Expression
1 cmt2.b 
 |-  B = ( Base ` K )
2 cmt2.o 
 |-  ._|_ = ( oc ` K )
3 cmt2.c 
 |-  C = ( cm ` K )
4 omllat 
 |-  ( K e. OML -> K e. Lat )
5 4 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
6 eqid 
 |-  ( meet ` K ) = ( meet ` K )
7 1 6 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) Y ) e. B )
8 4 7 syl3an1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) Y ) e. B )
9 simp2 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
10 omlop 
 |-  ( K e. OML -> K e. OP )
11 10 3ad2ant1 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OP )
12 simp3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
13 1 2 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
14 11 12 13 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
15 1 6 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X ( meet ` K ) ( ._|_ ` Y ) ) e. B )
16 5 9 14 15 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) ( ._|_ ` Y ) ) e. B )
17 eqid 
 |-  ( join ` K ) = ( join ` K )
18 1 17 latjcom 
 |-  ( ( K e. Lat /\ ( X ( meet ` K ) Y ) e. B /\ ( X ( meet ` K ) ( ._|_ ` Y ) ) e. B ) -> ( ( X ( meet ` K ) Y ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` Y ) ) ) = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) Y ) ) )
19 5 8 16 18 syl3anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ( meet ` K ) Y ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` Y ) ) ) = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) Y ) ) )
20 1 2 opococ 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
21 11 12 20 syl2anc 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
22 21 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) = ( X ( meet ` K ) Y ) )
23 22 oveq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) ) = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) Y ) ) )
24 19 23 eqtr4d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X ( meet ` K ) Y ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` Y ) ) ) = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) ) )
25 24 eqeq2d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X = ( ( X ( meet ` K ) Y ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` Y ) ) ) <-> X = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
26 1 17 6 2 3 cmtvalN 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ( meet ` K ) Y ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` Y ) ) ) ) )
27 1 17 6 2 3 cmtvalN 
 |-  ( ( K e. OML /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X C ( ._|_ ` Y ) <-> X = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
28 14 27 syld3an3 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C ( ._|_ ` Y ) <-> X = ( ( X ( meet ` K ) ( ._|_ ` Y ) ) ( join ` K ) ( X ( meet ` K ) ( ._|_ ` ( ._|_ ` Y ) ) ) ) ) )
29 25 26 28 3bitr4d 
 |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X C ( ._|_ ` Y ) ) )