Theorem nnmass 3181

Description: Multiplication of natural numbers is associative. (This can be extended to all ordinals with a longer proof.) Theorem 4K(4) of [Enderton] p. 81.

Assertion

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

Proof of Theorem nnmass

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . . 7 |- (x = (/) -> ((A .o B) .o x) = ((A .o B) .o (/)))
2		opreq2 3007	. . . . . . . 8 |- (x = (/) -> (B .o x) = (B .o (/)))
3	2	opreq2d 3013	. . . . . . 7 |- (x = (/) -> (A .o (B .o x)) = (A .o (B .o (/))))
4	1, 3	cleq12d 1115	. . . . . 6 |- (x = (/) -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o (/)) = (A .o (B .o (/)))))
5	4	imbi2d 464	. . . . 5 |- (x = (/) -> (((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 (/)) = (A .o (B .o (/))))))
6		opreq2 3007	. . . . . . 7 |- (x = y -> ((A .o B) .o x) = ((A .o B) .o y))
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	6, 8	cleq12d 1115	. . . . . 6 |- (x = y -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o y) = (A .o (B .o y))))
10	9	imbi2d 464	. . . . 5 |- (x = y -> (((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 y) = (A .o (B .o y)))))
11		opreq2 3007	. . . . . . 7 |- (x = suc y -> ((A .o B) .o x) = ((A .o B) .o suc y))
12		opreq2 3007	. . . . . . . 8 |- (x = suc y -> (B .o x) = (B .o suc y))
13	12	opreq2d 3013	. . . . . . 7 |- (x = suc y -> (A .o (B .o x)) = (A .o (B .o suc y)))
14	11, 13	cleq12d 1115	. . . . . 6 |- (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))))
15	14	imbi2d 464	. . . . 5 |- (x = suc y -> (((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 suc y) = (A .o (B .o suc y)))))
16		opreq2 3007	. . . . . . 7 |- (x = C -> ((A .o B) .o x) = ((A .o B) .o C))
17		opreq2 3007	. . . . . . . 8 |- (x = C -> (B .o x) = (B .o C))
18	17	opreq2d 3013	. . . . . . 7 |- (x = C -> (A .o (B .o x)) = (A .o (B .o C)))
19	16, 18	cleq12d 1115	. . . . . 6 |- (x = C -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o C) = (A .o (B .o C))))
20	19	imbi2d 464	. . . . 5 |- (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)))))
21		nnmcl 3173	. . . . . . 7 |- ((A e. om /\ B e. om) -> (A .o B) e. om)
22		nnm0 3167	. . . . . . 7 |- ((A .o B) e. om -> ((A .o B) .o (/)) = (/))
23	21, 22	syl 12	. . . . . 6 |- ((A e. om /\ B e. om) -> ((A .o B) .o (/)) = (/))
24		nnm0 3167	. . . . . . . 8 |- (B e. om -> (B .o (/)) = (/))
25	24	opreq2d 3013	. . . . . . 7 |- (B e. om -> (A .o (B .o (/))) = (A .o (/)))
26		nnm0 3167	. . . . . . 7 |- (A e. om -> (A .o (/)) = (/))
27	25, 26	sylan9eqr 1145	. . . . . 6 |- ((A e. om /\ B e. om) -> (A .o (B .o (/))) = (/))
28	23, 27	eqtr4d 1131	. . . . 5 |- ((A e. om /\ B e. om) -> ((A .o B) .o (/)) = (A .o (B .o (/))))
29		nnmsuc 3169	. . . . . . . . . . . . 13 |- (((A .o B) e. om /\ y e. om) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
30	29, 21	sylan 343	. . . . . . . . . . . 12 |- (((A e. om /\ B e. om) /\ y e. om) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
31	30	3impa 609	. . . . . . . . . . 11 |- ((A e. om /\ B e. om /\ y e. om) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
32		nnmsuc 3169	. . . . . . . . . . . . . 14 |- ((B e. om /\ y e. om) -> (B .o suc y) = ((B .o y) +o B))
33	32	3adant1 597	. . . . . . . . . . . . 13 |- ((A e. om /\ B e. om /\ y e. om) -> (B .o suc y) = ((B .o y) +o B))
34	33	opreq2d 3013	. . . . . . . . . . . 12 |- ((A e. om /\ B e. om /\ y e. om) -> (A .o (B .o suc y)) = (A .o ((B .o y) +o B)))
35		nndi 3180	. . . . . . . . . . . . . . . . . 18 |- ((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)))
36		nnmcl 3173	. . . . . . . . . . . . . . . . . 18 |- ((B e. om /\ y e. om) -> (B .o y) e. om)
37	35, 36	syl3an2 620	. . . . . . . . . . . . . . . . 17 |- ((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)))
38	37	3exp 611	. . . . . . . . . . . . . . . 16 |- (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)))))
39	38	exp3a 292	. . . . . . . . . . . . . . 15 |- (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))))))
40	39	com34 36	. . . . . . . . . . . . . 14 |- (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))))))
41	40	pm2.43d 59	. . . . . . . . . . . . 13 |- (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)))))
42	41	3imp 608	. . . . . . . . . . . 12 |- ((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)))
43	34, 42	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 .o B)))
44	31, 43	cleq12d 1115	. . . . . . . . . 10 |- ((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))))
45		opreq1 3006	. . . . . . . . . 10 |- (((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)))
46	44, 45	syl5bir 184	. . . . . . . . 9 |- ((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))))
47	46	3exp 611	. . . . . . . 8 |- (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))))))
48	47	com3r 35	. . . . . . 7 |- (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))))))
49	48	imp3a 279	. . . . . 6 |- (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)))))
50	49	a2d 15	. . . . 5 |- (y e. om -> (((A e. om /\ B e. om) -> ((A .o B) .o y) = (A .o (B .o y))) -> ((A e. om /\ B e. om) -> ((A .o B) .o suc y) = (A .o (B .o suc y