Metamath Proof Explorer


Theorem cmtvalN

Description: Equivalence for commutes relation. Definition of commutes in Kalmbach p. 20. ( cmbr analog.) (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cmtfval.b
 |-  B = ( Base ` K )
2 cmtfval.j
 |-  .\/ = ( join ` K )
3 cmtfval.m
 |-  ./\ = ( meet ` K )
4 cmtfval.o
 |-  ._|_ = ( oc ` K )
5 cmtfval.c
 |-  C = ( cm ` K )
6 1 2 3 4 5 cmtfvalN
 |-  ( K e. A -> C = { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )
7 df-3an
 |-  ( ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) <-> ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) )
8 7 opabbii
 |-  { <. x , y >. | ( x e. B /\ y e. B /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) }
9 6 8 eqtrdi
 |-  ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )
10 9 breqd
 |-  ( K e. A -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y ) )
11 10 3ad2ant1
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y ) )
12 df-br
 |-  ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } )
13 id
 |-  ( x = X -> x = X )
14 oveq1
 |-  ( x = X -> ( x ./\ y ) = ( X ./\ y ) )
15 oveq1
 |-  ( x = X -> ( x ./\ ( ._|_ ` y ) ) = ( X ./\ ( ._|_ ` y ) ) )
16 14 15 oveq12d
 |-  ( x = X -> ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) )
17 13 16 eqeq12d
 |-  ( x = X -> ( x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) <-> X = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) ) )
18 oveq2
 |-  ( y = Y -> ( X ./\ y ) = ( X ./\ Y ) )
19 fveq2
 |-  ( y = Y -> ( ._|_ ` y ) = ( ._|_ ` Y ) )
20 19 oveq2d
 |-  ( y = Y -> ( X ./\ ( ._|_ ` y ) ) = ( X ./\ ( ._|_ ` Y ) ) )
21 18 20 oveq12d
 |-  ( y = Y -> ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) )
22 21 eqeq2d
 |-  ( y = Y -> ( X = ( ( X ./\ y ) .\/ ( X ./\ ( ._|_ ` y ) ) ) <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
23 17 22 opelopab2
 |-  ( ( X e. B /\ Y e. B ) -> ( <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
24 12 23 syl5bb
 |-  ( ( X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
25 24 3adant1
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )
26 11 25 bitrd
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X = ( ( X ./\ Y ) .\/ ( X ./\ ( ._|_ ` Y ) ) ) ) )