Metamath Proof Explorer

Theorem nndi

Description: Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
2 1 oveq2d 
 |-  ( x = C -> ( A .o ( B +o x ) ) = ( A .o ( B +o C ) ) )
3 oveq2 
 |-  ( x = C -> ( A .o x ) = ( A .o C ) )
4 3 oveq2d 
 |-  ( x = C -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o C ) ) )
5 2 4 eqeq12d 
 |-  ( x = C -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) )
6 5 imbi2d 
 |-  ( x = C -> ( ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) ) )
7 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
8 7 oveq2d 
 |-  ( x = (/) -> ( A .o ( B +o x ) ) = ( A .o ( B +o (/) ) ) )
9 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
10 9 oveq2d 
 |-  ( x = (/) -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o (/) ) ) )
11 8 10 eqeq12d 
 |-  ( x = (/) -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o (/) ) ) = ( ( A .o B ) +o ( A .o (/) ) ) ) )
12 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
13 12 oveq2d 
 |-  ( x = y -> ( A .o ( B +o x ) ) = ( A .o ( B +o y ) ) )
14 oveq2 
 |-  ( x = y -> ( A .o x ) = ( A .o y ) )
15 14 oveq2d 
 |-  ( x = y -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o y ) ) )
16 13 15 eqeq12d 
 |-  ( x = y -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) )
17 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
18 17 oveq2d 
 |-  ( x = suc y -> ( A .o ( B +o x ) ) = ( A .o ( B +o suc y ) ) )
19 oveq2 
 |-  ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
20 19 oveq2d 
 |-  ( x = suc y -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o suc y ) ) )
21 18 20 eqeq12d 
 |-  ( x = suc y -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) )
22 nna0 
 |-  ( B e. _om -> ( B +o (/) ) = B )
23 22 adantl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( B +o (/) ) = B )
24 23 oveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o (/) ) ) = ( A .o B ) )
25 nnmcl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )
26 nna0 
 |-  ( ( A .o B ) e. _om -> ( ( A .o B ) +o (/) ) = ( A .o B ) )
27 25 26 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) +o (/) ) = ( A .o B ) )
28 24 27 eqtr4d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o (/) ) ) = ( ( A .o B ) +o (/) ) )
29 nnm0 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )
30 29 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o (/) ) = (/) )
31 30 oveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A .o B ) +o ( A .o (/) ) ) = ( ( A .o B ) +o (/) ) )
32 28 31 eqtr4d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o (/) ) ) = ( ( A .o B ) +o ( A .o (/) ) ) )
33 oveq1 
 |-  ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( ( A .o ( B +o y ) ) +o A ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) )
34 nnasuc 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
35 34 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
36 35 oveq2d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o ( B +o suc y ) ) = ( A .o suc ( B +o y ) ) )
37 nnacl 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o y ) e. _om )
38 nnmsuc 
 |-  ( ( A e. _om /\ ( B +o y ) e. _om ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
39 37 38 sylan2 
 |-  ( ( A e. _om /\ ( B e. _om /\ y e. _om ) ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
40 39 3impb 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
41 36 40 eqtrd 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o ( B +o suc y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
42 nnmsuc 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
43 42 3adant2 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
44 43 oveq2d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( A .o B ) +o ( A .o suc y ) ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
45 nnmcl 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A .o y ) e. _om )
46 nnaass 
 |-  ( ( ( A .o B ) e. _om /\ ( A .o y ) e. _om /\ A e. _om ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
47 25 46 syl3an1 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( A .o y ) e. _om /\ A e. _om ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
48 45 47 syl3an2 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( A e. _om /\ y e. _om ) /\ A e. _om ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
49 48 3exp 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A e. _om /\ y e. _om ) -> ( A e. _om -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) )
50 49 exp4b 
 |-  ( A e. _om -> ( B e. _om -> ( A e. _om -> ( y e. _om -> ( A e. _om -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) ) )
51 50 pm2.43a 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( A e. _om -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) )
52 51 com4r 
 |-  ( A e. _om -> ( A e. _om -> ( B e. _om -> ( y e. _om -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) )
53 52 pm2.43i 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) )
54 53 3imp 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
55 44 54 eqtr4d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( A .o B ) +o ( A .o suc y ) ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) )
56 41 55 eqeq12d 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) <-> ( ( A .o ( B +o y ) ) +o A ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) ) )
57 33 56 imbitrrid 
 |-  ( ( A e. _om /\ B e. _om /\ y e. _om ) -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) )
58 57 3exp 
 |-  ( A e. _om -> ( B e. _om -> ( y e. _om -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) ) )
59 58 com3r 
 |-  ( y e. _om -> ( A e. _om -> ( B e. _om -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) ) )
60 59 impd 
 |-  ( y e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) )
61 11 16 21 32 60 finds2 
 |-  ( x e. _om -> ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) )
62 6 61 vtoclga 
 |-  ( C e. _om -> ( ( A e. _om /\ B e. _om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) )
63 62 expdcom 
 |-  ( A e. _om -> ( B e. _om -> ( C e. _om -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) ) )
64 63 3imp 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )