Theorem nndi 3180

Description: Distributive law for natural numbers. (This can be extended to all ordinals with a longer proof.) Theorem 4K(3) of [Enderton] p. 81.

Assertion

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

Proof of Theorem nndi

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . . . 8 |- (x = (/) -> (B +o x) = (B +o (/)))
2	1	opreq2d 3013	. . . . . . 7 |- (x = (/) -> (A .o (B +o x)) = (A .o (B +o (/))))
3		opreq2 3007	. . . . . . . 8 |- (x = (/) -> (A .o x) = (A .o (/)))
4	3	opreq2d 3013	. . . . . . 7 |- (x = (/) -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o (/))))
5	2, 4	cleq12d 1115	. . . . . 6 |- (x = (/) -> ((A .o (B +o x)) = ((A .o B) +o (A .o x)) <-> (A .o (B +o (/))) = ((A .o B) +o (A .o (/)))))
6	5	imbi2d 464	. . . . 5 |- (x = (/) -> (((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 (/))) = ((A .o B) +o (A .o (/))))))
7		opreq2 3007	. . . . . . . 8 |- (x = y -> (B +o x) = (B +o y))
8	7	opreq2d 3013	. . . . . . 7 |- (x = y -> (A .o (B +o x)) = (A .o (B +o y)))
9		opreq2 3007	. . . . . . . 8 |- (x = y -> (A .o x) = (A .o y))
10	9	opreq2d 3013	. . . . . . 7 |- (x = y -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o y)))
11	8, 10	cleq12d 1115	. . . . . 6 |- (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))))
12	11	imbi2d 464	. . . . 5 |- (x = y -> (((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 y)) = ((A .o B) +o (A .o y)))))
13		opreq2 3007	. . . . . . . 8 |- (x = suc y -> (B +o x) = (B +o suc y))
14	13	opreq2d 3013	. . . . . . 7 |- (x = suc y -> (A .o (B +o x)) = (A .o (B +o suc y)))
15		opreq2 3007	. . . . . . . 8 |- (x = suc y -> (A .o x) = (A .o suc y))
16	15	opreq2d 3013	. . . . . . 7 |- (x = suc y -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o suc y)))
17	14, 16	cleq12d 1115	. . . . . 6 |- (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))))
18	17	imbi2d 464	. . . . 5 |- (x = suc y -> (((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 suc y)) = ((A .o B) +o (A .o suc y)))))
19		opreq2 3007	. . . . . . . 8 |- (x = C -> (B +o x) = (B +o C))
20	19	opreq2d 3013	. . . . . . 7 |- (x = C -> (A .o (B +o x)) = (A .o (B +o C)))
21		opreq2 3007	. . . . . . . 8 |- (x = C -> (A .o x) = (A .o C))
22	21	opreq2d 3013	. . . . . . 7 |- (x = C -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o C)))
23	20, 22	cleq12d 1115	. . . . . 6 |- (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))))
24	23	imbi2d 464	. . . . 5 |- (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)))))
25		nnmcl 3173	. . . . . . 7 |- ((A e. om /\ B e. om) -> (A .o B) e. om)
26		nna0 3166	. . . . . . 7 |- ((A .o B) e. om -> ((A .o B) +o (/)) = (A .o B))
27	25, 26	syl 12	. . . . . 6 |- ((A e. om /\ B e. om) -> ((A .o B) +o (/)) = (A .o B))
28		pm3.26 256	. . . . . . . 8 |- ((A e. om /\ B e. om) -> A e. om)
29		nnont 2379	. . . . . . . 8 |- (A e. om -> A e. On)
30		om0 3125	. . . . . . . 8 |- (A e. On -> (A .o (/)) = (/))
31	28, 29, 30	3syl 21	. . . . . . 7 |- ((A e. om /\ B e. om) -> (A .o (/)) = (/))
32	31	opreq2d 3013	. . . . . 6 |- ((A e. om /\ B e. om) -> ((A .o B) +o (A .o (/))) = ((A .o B) +o (/)))
33		nna0 3166	. . . . . . . 8 |- (B e. om -> (B +o (/)) = B)
34	33	adantl 305	. . . . . . 7 |- ((A e. om /\ B e. om) -> (B +o (/)) = B)
35	34	opreq2d 3013	. . . . . 6 |- ((A e. om /\ B e. om) -> (A .o (B +o (/))) = (A .o B))
36	27, 32, 35	3eqtr4rd 1135	. . . . 5 |- ((A e. om /\ B e. om) -> (A .o (B +o (/))) = ((A .o B) +o (A .o (/))))
37		nnasuc 3168	. . . . . . . . . . . . . 14 |- ((B e. om /\ y e. om) -> (B +o suc y) = suc (B +o y))
38	37	3adant1 597	. . . . . . . . . . . . 13 |- ((A e. om /\ B e. om /\ y e. om) -> (B +o suc y) = suc (B +o y))
39	38	opreq2d 3013	. . . . . . . . . . . 12 |- ((A e. om /\ B e. om /\ y e. om) -> (A .o (B +o suc y)) = (A .o suc (B +o y)))
40		nnmsuc 3169	. . . . . . . . . . . . . 14 |- ((A e. om /\ (B +o y) e. om) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
41		nnacl 3172	. . . . . . . . . . . . . 14 |- ((B e. om /\ y e. om) -> (B +o y) e. om)
42	40, 41	sylan2 346	. . . . . . . . . . . . 13 |- ((A e. om /\ (B e. om /\ y e. om)) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
43	42	3impb 610	. . . . . . . . . . . 12 |- ((A e. om /\ B e. om /\ y e. om) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
44	39, 43	eqtrd 1128	. . . . . . . . . . 11 |- ((A e. om /\ B e. om /\ y e. om) -> (A .o (B +o suc y)) = ((A .o (B +o y)) +o A))
45		nnmsuc 3169	. . . . . . . . . . . . . 14 |- ((A e. om /\ y e. om) -> (A .o suc y) = ((A .o y) +o A))
46	45	3adant2 598	. . . . . . . . . . . . 13 |- ((A e. om /\ B e. om /\ y e. om) -> (A .o suc y) = ((A .o y) +o A))
47	46	opreq2d 3013	. . . . . . . . . . . 12 |- ((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)))
48		nnaass 3179	. . . . . . . . . . . . . . . . . . . 20 |- (((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)))
49	48, 25	syl3an1 619	. . . . . . . . . . . . . . . . . . 19 |- (((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)))
50		nnmcl 3173	. . . . . . . . . . . . . . . . . . 19 |- ((A e. om /\ y e. om) -> (A .o y) e. om)
51	49, 50	syl3an2 620	. . . . . . . . . . . . . . . . . 18 |- (((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)))
52	51	3exp 611	. . . . . . . . . . . . . . . . 17 |- ((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)))))
53	52	exp4b 296	. . . . . . . . . . . . . . . 16 |- (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)))))))
54	53	pm2.43a 60	. . . . . . . . . . . . . . 15 |- (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))))))
55	54	com4r 41	. . . . . . . . . . . . . 14 |- (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 ((