Theorem omass 4217

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 3975	. . . . . 6 |- (x = (/) -> ((A .o B) .o x) = ((A .o B) .o (/)))
2		opreq2 3975	. . . . . . 7 |- (x = (/) -> (B .o x) = (B .o (/)))
3	2	opreq2d 3982	. . . . . 6 |- (x = (/) -> (A .o (B .o x)) = (A .o (B .o (/))))
4	1, 3	eqeq12d 1492	. . . . 5 |- (x = (/) -> (((A .o B) .o x) = (A .o (B .o x)) <-> ((A .o B) .o (/)) = (A .o (B .o (/)))))
5		opreq2 3975	. . . . . 6 |- (x = y -> ((A .o B) .o x) = ((A .o B) .o y))
6		opreq2 3975	. . . . . . 7 |- (x = y -> (B .o x) = (B .o y))
7	6	opreq2d 3982	. . . . . 6 |- (x = y -> (A .o (B .o x)) = (A .o (B .o y)))
8	5, 7	eqeq12d 1492	. . . . 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 3975	. . . . . 6 |- (x = suc y -> ((A .o B) .o x) = ((A .o B) .o suc y))
10		opreq2 3975	. . . . . . 7 |- (x = suc y -> (B .o x) = (B .o suc y))
11	10	opreq2d 3982	. . . . . 6 |- (x = suc y -> (A .o (B .o x)) = (A .o (B .o suc y)))
12	9, 11	eqeq12d 1492	. . . . 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 3975	. . . . . 6 |- (x = C -> ((A .o B) .o x) = ((A .o B) .o C))
14		opreq2 3975	. . . . . . 7 |- (x = C -> (B .o x) = (B .o C))
15	14	opreq2d 3982	. . . . . 6 |- (x = C -> (A .o (B .o x)) = (A .o (B .o C)))
16	13, 15	eqeq12d 1492	. . . . 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 4177	. . . . . . 7 |- ((A e. On /\ B e. On) -> (A .o B) e. On)
18		om0 4162	. . . . . . 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 4162	. . . . . . . 8 |- (B e. On -> (B .o (/)) = (/))
21	20	opreq2d 3982	. . . . . . 7 |- (B e. On -> (A .o (B .o (/))) = (A .o (/)))
22		om0 4162	. . . . . . 7 |- (A e. On -> (A .o (/)) = (/))
23	21, 22	sylan9eqr 1532	. . . . . 6 |- ((A e. On /\ B e. On) -> (A .o (B .o (/))) = (/))
24	19, 23	eqtr4d 1513	. . . . 5 |- ((A e. On /\ B e. On) -> ((A .o B) .o (/)) = (A .o (B .o (/))))
25		omsuc 4171	. . . . . . . . . . . 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 450	. . . . . . . . . . 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 830	. . . . . . . . . 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 4171	. . . . . . . . . . . . 13 |- ((B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
29	28	3adant1 799	. . . . . . . . . . . 12 |- ((A e. On /\ B e. On /\ y e. On) -> (B .o suc y) = ((B .o y) +o B))
30	29	opreq2d 3982	. . . . . . . . . . 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 4216	. . . . . . . . . . . . . . . . 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 4177	. . . . . . . . . . . . . . . . 17 |- ((B e. On /\ y e. On) -> (B .o y) e. On)
33	31, 32	syl3an2 862	. . . . . . . . . . . . . . . 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 834	. . . . . . . . . . . . . . 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 376	. . . . . . . . . . . . . 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 829	. . . . . . . . . . 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 1510	. . . . . . . . . 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 1492	. . . . . . . . 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 3974	. . . . . . . . 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 834	. . . . . . 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 1816	. . . . . . . . . . . . . . 15 |- x e. V
47		omlim 4174	. . . . . . . . . . . . . . 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 711	. . . . . . . . . . . . . 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 438	. . . . . . . . . . . . . 14 |- ((B e. On /\ A e. On) -> (A .o B) e. On)
50	48, 49	sylan 450	. . . . . . . . . . . . 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 491	. . . . . . . . . . . 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 406	. . . . . . . . . . 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 2582	. . . . . . . . . . . 12 |- (A.y e. x ((A .o B) .o y) = (A .o (B .o y)) -> U_y e. x ((A .o B) .o