Theorem odi 4194

Description: Distributive law for ordinal arithmetic. Proposition 8.25 of [TakeutiZaring] p. 64. Warning: The HTML proof page is 3/4 megabyte in size.

Assertion

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

Proof of Theorem odi

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . . 7 |- (x = (/) -> (B +o x) = (B +o (/)))
2	1	opreq2d 3961	. . . . . 6 |- (x = (/) -> (A .o (B +o x)) = (A .o (B +o (/))))
3		opreq2 3954	. . . . . . 7 |- (x = (/) -> (A .o x) = (A .o (/)))
4	3	opreq2d 3961	. . . . . 6 |- (x = (/) -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o (/))))
5	2, 4	eqeq12d 1481	. . . . 5 |- (x = (/) -> ((A .o (B +o x)) = ((A .o B) +o (A .o x)) <-> (A .o (B +o (/))) = ((A .o B) +o (A .o (/)))))
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		opreq2 3954	. . . . . . 7 |- (x = y -> (A .o x) = (A .o y))
9	8	opreq2d 3961	. . . . . 6 |- (x = y -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o y)))
10	7, 9	eqeq12d 1481	. . . . 5 |- (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))))
11		opreq2 3954	. . . . . . 7 |- (x = suc y -> (B +o x) = (B +o suc y))
12	11	opreq2d 3961	. . . . . 6 |- (x = suc y -> (A .o (B +o x)) = (A .o (B +o suc y)))
13		opreq2 3954	. . . . . . 7 |- (x = suc y -> (A .o x) = (A .o suc y))
14	13	opreq2d 3961	. . . . . 6 |- (x = suc y -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o suc y)))
15	12, 14	eqeq12d 1481	. . . . 5 |- (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))))
16		opreq2 3954	. . . . . . 7 |- (x = C -> (B +o x) = (B +o C))
17	16	opreq2d 3961	. . . . . 6 |- (x = C -> (A .o (B +o x)) = (A .o (B +o C)))
18		opreq2 3954	. . . . . . 7 |- (x = C -> (A .o x) = (A .o C))
19	18	opreq2d 3961	. . . . . 6 |- (x = C -> ((A .o B) +o (A .o x)) = ((A .o B) +o (A .o C)))
20	17, 19	eqeq12d 1481	. . . . 5 |- (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))))
21		omcl 4155	. . . . . . 7 |- ((A e. On /\ B e. On) -> (A .o B) e. On)
22		oa0 4139	. . . . . . 7 |- ((A .o B) e. On -> ((A .o B) +o (/)) = (A .o B))
23	21, 22	syl 10	. . . . . 6 |- ((A e. On /\ B e. On) -> ((A .o B) +o (/)) = (A .o B))
24		om0 4140	. . . . . . . 8 |- (A e. On -> (A .o (/)) = (/))
25	24	adantr 389	. . . . . . 7 |- ((A e. On /\ B e. On) -> (A .o (/)) = (/))
26	25	opreq2d 3961	. . . . . 6 |- ((A e. On /\ B e. On) -> ((A .o B) +o (A .o (/))) = ((A .o B) +o (/)))
27		oa0 4139	. . . . . . . 8 |- (B e. On -> (B +o (/)) = B)
28	27	adantl 388	. . . . . . 7 |- ((A e. On /\ B e. On) -> (B +o (/)) = B)
29	28	opreq2d 3961	. . . . . 6 |- ((A e. On /\ B e. On) -> (A .o (B +o (/))) = (A .o B))
30	23, 26, 29	3eqtr4rd 1510	. . . . 5 |- ((A e. On /\ B e. On) -> (A .o (B +o (/))) = ((A .o B) +o (A .o (/))))
31		oasuc 4147	. . . . . . . . . . . . 13 |- ((B e. On /\ y e. On) -> (B +o suc y) = suc (B +o y))
32	31	3adant1 795	. . . . . . . . . . . 12 |- ((A e. On /\ B e. On /\ y e. On) -> (B +o suc y) = suc (B +o y))
33	32	opreq2d 3961	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o (B +o suc y)) = (A .o suc (B +o y)))
34		omsuc 4149	. . . . . . . . . . . . 13 |- ((A e. On /\ (B +o y) e. On) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
35		oacl 4154	. . . . . . . . . . . . 13 |- ((B e. On /\ y e. On) -> (B +o y) e. On)
36	34, 35	sylan2 451	. . . . . . . . . . . 12 |- ((A e. On /\ (B e. On /\ y e. On)) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
37	36	3impb 827	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o suc (B +o y)) = ((A .o (B +o y)) +o A))
38	33, 37	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))
39		omsuc 4149	. . . . . . . . . . . . 13 |- ((A e. On /\ y e. On) -> (A .o suc y) = ((A .o y) +o A))
40	39	3adant2 796	. . . . . . . . . . . 12 |- ((A e. On /\ B e. On /\ y e. On) -> (A .o suc y) = ((A .o y) +o A))
41	40	opreq2d 3961	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> ((A .o B) +o (A .o suc y)) = ((A .o B) +o ((A .o y) +o A)))
42		oaass 4179	. . . . . . . . . . . . . . . . . . 19 |- (((A .o B) e. On /\ (A .o y) e. On /\ A e. On) -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))
43	42, 21	syl3an1 857	. . . . . . . . . . . . . . . . . 18 |- (((A e. On /\ B e. On) /\ (A .o y) e. On /\ A e. On) -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))
44		omcl 4155	. . . . . . . . . . . . . . . . . 18 |- ((A e. On /\ y e. On) -> (A .o y) e. On)
45	43, 44	syl3an2 858	. . . . . . . . . . . . . . . . 17 |- (((A e. On /\ B e. On) /\ (A e. On /\ y e. On) /\ A e. On) -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))
46	45	3exp 830	. . . . . . . . . . . . . . . 16 |- ((A e. On /\ B e. On) -> ((A e. On /\ y e. On) -> (A e. On -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))))
47	46	exp4b 379	. . . . . . . . . . . . . . 15 |- (A e. On -> (B e. On -> (A e. On -> (y e. On -> (A e. On -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))))))
48	47	pm2.43a 66	. . . . . . . . . . . . . 14 |- (A e. On -> (B e. On -> (y e. On -> (A e. On -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A))))))
49	48	com4r 41	. . . . . . . . . . . . 13 |- (A e. On -> (A e. On -> (B e. On -> (y e. On -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A))))))
50	49	pm2.43i 64	. . . . . . . . . . . 12 |- (A e. On -> (B e. On -> (y e. On -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))))
51	50	3imp 825	. . . . . . . . . . 11 |- ((A e. On /\ B e. On /\ y e. On) -> (((A .o B) +o (A .o y)) +o A) = ((A .o B) +o ((A .o y) +o A)))
52	41, 51	eqtr4d 1502	. . . . . . . . . 10 |- ((A e. On /\ B e. On /\ y e. On) -> ((A .o B) +o (A .o suc y)) = (((A .o B) +o (A .o y)) +o A))
53	38, 52	eqeq12d 1481	. . . . . . . . 9 |- ((A e. On /\ B e. On /\ y e. On) -> ((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)))
54		opreq1 3953	. . . . . . . . 9 |- ((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))
55	53, 54	syl5bir 210	. . .