Theorem omass 4195

Description: Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65.

Assertion

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

Proof of Theorem omass

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . 6 |- (x = (/) -> ((A .o B) .o x) = ((A .o B) .o (/)))
2		opreq2 3954	. . . . . . 7 |- (x = (/) -> (B .o x) = (B .o (/)))
3	2	opreq2d 3961	. . . . . 6 |- (x = (/) -> (A .o (B .o x)) = (A .o (B .o (/))))
4	1, 3	eqeq12d 1481	. . . . 5 |- (x = (/) -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o (/)) = (A .o (B .o (/)))))
5		opreq2 3954	. . . . . 6 |- (x = y -> ((A .o B) .o x) = ((A .o B) .o y))
6		opreq2 3954	. . . . . . 7 |- (x = y -> (B .o x) = (B .o y))
7	6	opreq2d 3961	. . . . . 6 |- (x = y -> (A .o (B .o x)) = (A .o (B .o y)))
8	5, 7	eqeq12d 1481	. . . . 5 |- (x = y -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o y) = (A .o (B .o y))))
9		opreq2 3954	. . . . . 6 |- (x = suc y -> ((A .o B) .o x) = ((A .o B) .o suc y))
10		opreq2 3954	. . . . . . 7 |- (x = suc y -> (B .o x) = (B .o suc y))
11	10	opreq2d 3961	. . . . . 6 |- (x = suc y -> (A .o (B .o x)) = (A .o (B .o suc y)))
12	9, 11	eqeq12d 1481	. . . . 5 |- (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))))
13		opreq2 3954	. . . . . 6 |- (x = C -> ((A .o B) .o x) = ((A .o B) .o C))
14		opreq2 3954	. . . . . . 7 |- (x = C -> (B .o x) = (B .o C))
15	14	opreq2d 3961	. . . . . 6 |- (x = C -> (A .o (B .o x)) = (A .o (B .o C)))
16	13, 15	eqeq12d 1481	. . . . 5 |- (x = C -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o C) = (A .o (B .o C))))
17		omcl 4155	. . . . . . 7 |- ((A e. On /\ B e. On) -> (A .o B) e. On)
18		om0 4140	. . . . . . 7 |- ((A .o B) e. On -> ((A .o B) .o (/)) = (/))
19	17, 18	syl 10	. . . . . 6 |- ((A e. On /\ B e. On) -> ((A .o B) .o (/)) = (/))
20		om0 4140	. . . . . . . 8 |- (B e. On -> (B .o (/)) = (/))
21	20	opreq2d 3961	. . . . . . 7 |- (B e. On -> (A .o (B .o (/))) = (A .o (/)))
22		om0 4140	. . . . . . 7 |- (A e. On -> (A .o (/)) = (/))
23	21, 22	sylan9eqr 1521	. . . . . 6 |- ((A e. On /\ B e. On) -> (A .o (B .o (/))) = (/))
24	19, 23	eqtr4d 1502	. . . . 5 |- ((A e. On /\ B e. On) -> ((A .o B) .o (/)) = (A .o (B .o (/))))
25		omsuc 4149	. . . . . . . . . . . 12 |- (((A .o B) e. On /\ y e. On) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
26	25, 17	sylan 448	. . . . . . . . . . 11 |- (((A e. On /\ B e. On) /\ y e. On) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
27	26	3impa 826	. . . . . . . . . 10 |- ((A e. On /\ B e. On /\ y e. On) -> ((A .o B) .o suc y) = (((A .o B) .o y) +o (A .o B)))
28		omsuc 4149	. . . . . . . . . . . . 13 |- ((B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
29	28	3adant1 795	. . . . . . . . . . . 12 |- ((A e. On /\ B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
30	29	opreq2d 3961	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o (B .o suc y)) = (A .o ((B .o y) +o B)))
31		odi 4194	. . . . . . . . . . . . . . . . 17 |- ((A e. On /\ (B .o y) e. On /\ B e. On) -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B)))
32		omcl 4155	. . . . . . . . . . . . . . . . 17 |- ((B e. On /\ y e. On) -> (B .o y) e. On)
33	31, 32	syl3an2 858	. . . . . . . . . . . . . . . 16 |- ((A e. On /\ (B e. On /\ y e. On) /\ B e. On) -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B)))
34	33	3exp 830	. . . . . . . . . . . . . . 15 |- (A e. On -> ((B e. On /\ y e. On) -> (B e. On -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B)))))
35	34	exp3a 375	. . . . . . . . . . . . . 14 |- (A e. On -> (B e. On -> (y e. On -> (B e. On -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B))))))
36	35	com34 36	. . . . . . . . . . . . 13 |- (A e. On -> (B e. On -> (B e. On -> (y e. On -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B))))))
37	36	pm2.43d 65	. . . . . . . . . . . 12 |- (A e. On -> (B e. On -> (y e. On -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B)))))
38	37	3imp 825	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o ((B .o y) +o B)) = ((A .o (B .o y)) +o (A .o B)))
39	30, 38	eqtrd 1499	. . . . . . . . . 10 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o (B .o suc y)) = ((A .o (B .o y)) +o (A .o B)))
40	27, 39	eqeq12d 1481	. . . . . . . . 9 |- ((A e. On /\ B e. On /\ y e. On) -> (((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))))
41		opreq1 3953	. . . . . . . . 9 |- (((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)))
42	40, 41	syl5bir 210	. . . . . . . 8 |- ((A e. On /\ B e. On /\ y e. On) -> (((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 830	. . . . . . 7 |- (A e. On -> (B e. On -> (y e. On -> (((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 35	. . . . . 6 |- (y e. On -> (A e. On -> (B e. On -> (((A .o B) .o y) = (A .o (B .o y)) -> ((A .o B) .o suc y) = (A .o (B .o suc y))))))
45	44	imp3a 361	. . . . 5 |- (y e. On -> ((A e. On /\ B e. On) -> (((A .o B) .o y) = (A .o (B .o y)) -> ((A .o B) .o suc y) = (A .o (B .o suc y)))))
46		visset 1804	. . . . . . . . . . . . . . 15 |- x e. V
47		omlim 4152	. . . . . . . . . . . . . . 15 |- (((A .o B) e. On /\ (x e. V /\ Lim x)) -> ((A .o B) .o x) = U_y e. x ((A .o B) .o y))
48	46, 47	mpanr1 707	. . . . . . . . . . . . . 14 |- (((A .o B) e. On /\ Lim x) -> ((A .o B) .o x) = U_y e. x ((A .o B) .o y))
49	17	ancoms 436	. . . . . . . . . . . . . 14 |- ((B e. On /\ A e. On) -> (A .o B) e. On)
50	48, 49	sylan 448	. . . . . . . . . . . . 13 |- (((B e. On /\ A e. On) /\ Lim x) -> ((A .o B) .o x) = U_y e. x ((A .o B) .o y))
51	50	an1rs 488	. . . . . . . . . . . 12 |- (((B e. On /\ Lim x) /\ A e. On) -> ((A .o B) .o x) = U_y e. x ((A .o B) .o y))
52	51	ad2antrr 404	. . . . . . . . . . 11 |- (((((B e. On /\ Lim x) /\ A e. On) /\ (/) e. B) /\ A.y e. x ((A .o B) .o y) = (A .o (B .o y))) -> ((A .o B) .o x) = U_y e. x ((A .o B) .o y))
53		iuneq2 2568	. . . . . . . . . . . 12 |- (A.y e. x ((A .o B) .o y) = (A .o (B .o y)) -> U_y e. x ((A .o B) .o y