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

Metamath Proof Explorer

Theorem nnmass

Description: Multiplication of natural numbers is associative. Theorem 4K(4) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnmass 
|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = C -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o C ) )
2 oveq2 
 |-  ( x = C -> ( B .o x ) = ( B .o C ) )
3 2 oveq2d 
 |-  ( x = C -> ( A .o ( B .o x ) ) = ( A .o ( B .o C ) ) )
4 1 3 eqeq12d 
 |-  ( x = C -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) )
5 4 imbi2d 
 |-  ( x = C -> ( ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) ) )
6 oveq2 
 |-  ( x = (/) -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o (/) ) )
7 oveq2 
 |-  ( x = (/) -> ( B .o x ) = ( B .o (/) ) )
8 7 oveq2d 
 |-  ( x = (/) -> ( A .o ( B .o x ) ) = ( A .o ( B .o (/) ) ) )
9 6 8 eqeq12d 
 |-  ( x = (/) -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o (/) ) = ( A .o ( B .o (/) ) ) ) )
10 oveq2 
 |-  ( x = y -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o y ) )
11 oveq2 
 |-  ( x = y -> ( B .o x ) = ( B .o y ) )
12 11 oveq2d 
 |-  ( x = y -> ( A .o ( B .o x ) ) = ( A .o ( B .o y ) ) )
13 10 12 eqeq12d 
 |-  ( x = y -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) ) )
14 oveq2 
 |-  ( x = suc y -> ( ( A .o B ) .o x ) = ( ( A .o B ) .o suc y ) )
15 oveq2 
 |-  ( x = suc y -> ( B .o x ) = ( B .o suc y ) )
16 15 oveq2d 
 |-  ( x = suc y -> ( A .o ( B .o x ) ) = ( A .o ( B .o suc y ) ) )
17 14 16 eqeq12d 
 |-  ( x = suc y -> ( ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) <-> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) )
18 nnmcl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )
19 nnm0 
 |-  ( ( A .o B ) e. _om -> ( ( A .o B ) .o (/) ) = (/) )
20 18 19 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o (/) ) = (/) )
21 nnm0 
 |-  ( B e. _om -> ( B .o (/) ) = (/) )
22 21 oveq2d 
 |-  ( B e. _om -> ( A .o ( B .o (/) ) ) = ( A .o (/) ) )
23 nnm0 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )
24 22 23 sylan9eqr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o ( B .o (/) ) ) = (/) )
25 20 24 eqtr4d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o (/) ) = ( A .o ( B .o (/) ) ) )
26 oveq1 
 |-  ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( ( A .o B ) .o y ) +o ( A .o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
27 nnmsuc 
 |-  ( ( ( A .o B ) e. _om /\ y e. _om ) -> ( ( A .o B ) .o suc y ) = ( ( ( A .o B ) .o y ) +o ( A .o B ) ) )
28 18 27 stoic3 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( A .o B ) .o suc y ) = ( ( ( A .o B ) .o y ) +o ( A .o B ) ) )
29 nnmsuc 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
30 29 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
31 30 oveq2d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o ( B .o suc y ) ) = ( A .o ( ( B .o y ) +o B ) ) )
32 nnmcl 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B .o y ) e. _om )
33 nndi 
 |-  ( ( A e. _om /\ ( B .o y ) e. _om /\ B e. _om ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
34 32 33 syl3an2 
 |-  ( ( A e. _om /\ ( B e. _om /\ y e. _om ) /\ B e. _om ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
35 34 3exp 
 |-  ( A e. _om -> ( ( B e. _om /\ y e. _om ) -> ( B e. _om -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) )
36 35 expd 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( B e. _om -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) ) )
37 36 com34 
 |-  ( A e. _om -> ( B e. _om -> ( B e. _om -> ( y e. _om -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) ) )
38 37 pm2.43d 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) ) )
39 38 3imp 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o ( ( B .o y ) +o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
40 31 39 eqtrd 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o ( B .o suc y ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) )
41 28 40 eqeq12d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) <-> ( ( ( A .o B ) .o y ) +o ( A .o B ) ) = ( ( A .o ( B .o y ) ) +o ( A .o B ) ) ) )
42 26 41 imbitrrid 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) )
43 42 3exp 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) ) )
44 43 com3r 
 |-  ( y e. _om -> ( A e. _om -> ( B e. _om -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) ) )
45 44 impd 
 |-  ( y e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( ( A .o B ) .o y ) = ( A .o ( B .o y ) ) -> ( ( A .o B ) .o suc y ) = ( A .o ( B .o suc y ) ) ) ) )
46 9 13 17 25 45 finds2 
 |-  ( x e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o x ) = ( A .o ( B .o x ) ) ) )
47 5 46 vtoclga 
 |-  ( C e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) )
48 47 expdcom 
 |-  ( A e. _om -> ( B e. _om -> ( C e. _om -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) ) ) )
49 48 3imp 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )