Metamath Proof Explorer

Theorem omopth

Description: An ordered pair theorem for finite integers. Analogous to nn0opthi . (Contributed by Scott Fenton, 1-May-2012)

Ref Expression
Assertion omopth 
|- ( ( ( A e. _om /\ B e. _om ) /\ ( C e. _om /\ D e. _om ) ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( A +o B ) = ( if ( A e. _om , A , (/) ) +o B ) )
2 1 1 oveq12d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( A +o B ) .o ( A +o B ) ) = ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) )
3 2 oveq1d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) )
4 3 eqeq1d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) ) )
5 eqeq1 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( A = C <-> if ( A e. _om , A , (/) ) = C ) )
6 5 anbi1d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( A = C /\ B = D ) <-> ( if ( A e. _om , A , (/) ) = C /\ B = D ) ) )
7 4 6 bibi12d 
 |-  ( A = if ( A e. _om , A , (/) ) -> ( ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) ) <-> ( ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = C /\ B = D ) ) ) )
8 oveq2 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( if ( A e. _om , A , (/) ) +o B ) = ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) )
9 8 8 oveq12d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) = ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) )
10 id 
 |-  ( B = if ( B e. _om , B , (/) ) -> B = if ( B e. _om , B , (/) ) )
11 9 10 oveq12d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) = ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) )
12 11 eqeq1d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) ) )
13 eqeq1 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( B = D <-> if ( B e. _om , B , (/) ) = D ) )
14 13 anbi2d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( if ( A e. _om , A , (/) ) = C /\ B = D ) <-> ( if ( A e. _om , A , (/) ) = C /\ if ( B e. _om , B , (/) ) = D ) ) )
15 12 14 bibi12d 
 |-  ( B = if ( B e. _om , B , (/) ) -> ( ( ( ( ( if ( A e. _om , A , (/) ) +o B ) .o ( if ( A e. _om , A , (/) ) +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = C /\ B = D ) ) <-> ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = C /\ if ( B e. _om , B , (/) ) = D ) ) ) )
16 oveq1 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( C +o D ) = ( if ( C e. _om , C , (/) ) +o D ) )
17 16 16 oveq12d 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( ( C +o D ) .o ( C +o D ) ) = ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) )
18 17 oveq1d 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( ( ( C +o D ) .o ( C +o D ) ) +o D ) = ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) )
19 18 eqeq2d 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) ) )
20 eqeq2 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( if ( A e. _om , A , (/) ) = C <-> if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) ) )
21 20 anbi1d 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( ( if ( A e. _om , A , (/) ) = C /\ if ( B e. _om , B , (/) ) = D ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = D ) ) )
22 19 21 bibi12d 
 |-  ( C = if ( C e. _om , C , (/) ) -> ( ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = C /\ if ( B e. _om , B , (/) ) = D ) ) <-> ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = D ) ) ) )
23 oveq2 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( if ( C e. _om , C , (/) ) +o D ) = ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) )
24 23 23 oveq12d 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) = ( ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) .o ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) ) )
25 id 
 |-  ( D = if ( D e. _om , D , (/) ) -> D = if ( D e. _om , D , (/) ) )
26 24 25 oveq12d 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) = ( ( ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) .o ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) ) +o if ( D e. _om , D , (/) ) ) )
27 26 eqeq2d 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) <-> ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) .o ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) ) +o if ( D e. _om , D , (/) ) ) ) )
28 eqeq2 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( if ( B e. _om , B , (/) ) = D <-> if ( B e. _om , B , (/) ) = if ( D e. _om , D , (/) ) ) )
29 28 anbi2d 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = D ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = if ( D e. _om , D , (/) ) ) ) )
30 27 29 bibi12d 
 |-  ( D = if ( D e. _om , D , (/) ) -> ( ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o D ) .o ( if ( C e. _om , C , (/) ) +o D ) ) +o D ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = D ) ) <-> ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) .o ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) ) +o if ( D e. _om , D , (/) ) ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = if ( D e. _om , D , (/) ) ) ) ) )
31 peano1 
 |-  (/) e. _om
32 31 elimel 
 |-  if ( A e. _om , A , (/) ) e. _om
33 31 elimel 
 |-  if ( B e. _om , B , (/) ) e. _om
34 31 elimel 
 |-  if ( C e. _om , C , (/) ) e. _om
35 31 elimel 
 |-  if ( D e. _om , D , (/) ) e. _om
36 32 33 34 35 omopthi 
 |-  ( ( ( ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) .o ( if ( A e. _om , A , (/) ) +o if ( B e. _om , B , (/) ) ) ) +o if ( B e. _om , B , (/) ) ) = ( ( ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) .o ( if ( C e. _om , C , (/) ) +o if ( D e. _om , D , (/) ) ) ) +o if ( D e. _om , D , (/) ) ) <-> ( if ( A e. _om , A , (/) ) = if ( C e. _om , C , (/) ) /\ if ( B e. _om , B , (/) ) = if ( D e. _om , D , (/) ) ) )
37 7 15 22 30 36 dedth4h 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( C e. _om /\ D e. _om ) ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) ) )