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 ) ) ) ) )