MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  odi Unicode version

Theorem odi 7247
Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.)
Assertion
Ref Expression
odi

Proof of Theorem odi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6304 . . . . . 6
21oveq2d 6312 . . . . 5
3 oveq2 6304 . . . . . 6
43oveq2d 6312 . . . . 5
52, 4eqeq12d 2479 . . . 4
6 oveq2 6304 . . . . . 6
76oveq2d 6312 . . . . 5
8 oveq2 6304 . . . . . 6
98oveq2d 6312 . . . . 5
107, 9eqeq12d 2479 . . . 4
11 oveq2 6304 . . . . . 6
1211oveq2d 6312 . . . . 5
13 oveq2 6304 . . . . . 6
1413oveq2d 6312 . . . . 5
1512, 14eqeq12d 2479 . . . 4
16 oveq2 6304 . . . . . 6
1716oveq2d 6312 . . . . 5
18 oveq2 6304 . . . . . 6
1918oveq2d 6312 . . . . 5
2017, 19eqeq12d 2479 . . . 4
21 omcl 7205 . . . . . 6
22 oa0 7185 . . . . . 6
2321, 22syl 16 . . . . 5
24 om0 7186 . . . . . . 7
2524adantr 465 . . . . . 6
2625oveq2d 6312 . . . . 5
27 oa0 7185 . . . . . . 7
2827adantl 466 . . . . . 6
2928oveq2d 6312 . . . . 5
3023, 26, 293eqtr4rd 2509 . . . 4
31 oveq1 6303 . . . . . . . 8
32 oasuc 7193 . . . . . . . . . . . 12
33323adant1 1014 . . . . . . . . . . 11
3433oveq2d 6312 . . . . . . . . . 10
35 oacl 7204 . . . . . . . . . . . 12
36 omsuc 7195 . . . . . . . . . . . 12
3735, 36sylan2 474 . . . . . . . . . . 11
38373impb 1192 . . . . . . . . . 10
3934, 38eqtrd 2498 . . . . . . . . 9
40 omsuc 7195 . . . . . . . . . . . 12
41403adant2 1015 . . . . . . . . . . 11
4241oveq2d 6312 . . . . . . . . . 10
43 omcl 7205 . . . . . . . . . . . . . . . . 17
44 oaass 7229 . . . . . . . . . . . . . . . . . 18
4521, 44syl3an1 1261 . . . . . . . . . . . . . . . . 17
4643, 45syl3an2 1262 . . . . . . . . . . . . . . . 16
47463exp 1195 . . . . . . . . . . . . . . 15
4847exp4b 607 . . . . . . . . . . . . . 14
4948pm2.43a 49 . . . . . . . . . . . . 13
5049com4r 86 . . . . . . . . . . . 12
5150pm2.43i 47 . . . . . . . . . . 11
52513imp 1190 . . . . . . . . . 10
5342, 52eqtr4d 2501 . . . . . . . . 9
5439, 53eqeq12d 2479 . . . . . . . 8
5531, 54syl5ibr 221 . . . . . . 7
56553exp 1195 . . . . . 6
5756com3r 79 . . . . 5
5857impd 431 . . . 4
59 vex 3112 . . . . . . . . . . . . . 14
60 limelon 4946 . . . . . . . . . . . . . 14
6159, 60mpan 670 . . . . . . . . . . . . 13
62 oacl 7204 . . . . . . . . . . . . . . 15
63 om0r 7208 . . . . . . . . . . . . . . 15
6462, 63syl 16 . . . . . . . . . . . . . 14
65 om0r 7208 . . . . . . . . . . . . . . . 16
66 om0r 7208 . . . . . . . . . . . . . . . 16
6765, 66oveqan12d 6315 . . . . . . . . . . . . . . 15
68 0elon 4936 . . . . . . . . . . . . . . . 16
69 oa0 7185 . . . . . . . . . . . . . . . 16
7068, 69ax-mp 5 . . . . . . . . . . . . . . 15
7167, 70syl6req 2515 . . . . . . . . . . . . . 14
7264, 71eqtrd 2498 . . . . . . . . . . . . 13
7361, 72sylan2 474 . . . . . . . . . . . 12
7473ancoms 453 . . . . . . . . . . 11
75 oveq1 6303 . . . . . . . . . . . 12
76 oveq1 6303 . . . . . . . . . . . . 13
77 oveq1 6303 . . . . . . . . . . . . 13
7876, 77oveq12d 6314 . . . . . . . . . . . 12
7975, 78eqeq12d 2479 . . . . . . . . . . 11
8074, 79syl5ibr 221 . . . . . . . . . 10
8180expd 436 . . . . . . . . 9
8281com3r 79 . . . . . . . 8
8382imp 429 . . . . . . 7
8483a1dd 46 . . . . . 6
85 simplr 755 . . . . . . . . . . . . . . . . . . . 20
8662ancoms 453 . . . . . . . . . . . . . . . . . . . . 21
87 onelon 4908 . . . . . . . . . . . . . . . . . . . . 21
8886, 87sylan 471 . . . . . . . . . . . . . . . . . . . 20
89 ontri1 4917 . . . . . . . . . . . . . . . . . . . . 21
90 oawordex 7225 . . . . . . . . . . . . . . . . . . . . 21
9189, 90bitr3d 255 . . . . . . . . . . . . . . . . . . . 20
9285, 88, 91syl2anc 661 . . . . . . . . . . . . . . . . . . 19
93 oaord 7215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94933expb 1197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
95 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9694, 95sylan9bb 699 . . . . . . . . . . . . . . . . . . . . . . . . . 26
97 iba 503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9897adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9996, 98bitr3d 255 . . . . . . . . . . . . . . . . . . . . . . . . 25
10099an32s 804 . . . . . . . . . . . . . . . . . . . . . . . 24
101100biimpcd 224 . . . . . . . . . . . . . . . . . . . . . . 23
102101exp4c 608 . . . . . . . . . . . . . . . . . . . . . 22
103102com4r 86 . . . . . . . . . . . . . . . . . . . . 21
104103imp 429 . . . . . . . . . . . . . . . . . . . 20
105104reximdvai 2929 . . . . . . . . . . . . . . . . . . 19
10692, 105sylbid 215 . . . . . . . . . . . . . . . . . 18
107106orrd 378 . . . . . . . . . . . . . . . . 17
10861, 107sylanl1 650 . . . . . . . . . . . . . . . 16
109108adantlrl 719 . . . . . . . . . . . . . . 15
110109adantlr 714 . . . . . . . . . . . . . 14
111 0ellim 4945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
112 om00el 7244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
113112biimprd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114111, 113sylan2i 655 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11561, 114sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . 25
116115exp4b 607 . . . . . . . . . . . . . . . . . . . . . . . 24
117116com4r 86 . . . . . . . . . . . . . . . . . . . . . . 23
118117pm2.43a 49 . . . . . . . . . . . . . . . . . . . . . 22
119118imp31 432 . . . . . . . . . . . . . . . . . . . . 21
120119a1d 25 . . . . . . . . . . . . . . . . . . . 20
121120adantlrr 720 . . . . . . . . . . . . . . . . . . 19
122 omordi 7234 . . . . . . . . . . . . . . . . . . . . . 22
123122ancom1s 805 . . . . . . . . . . . . . . . . . . . . 21
124 onelss 4925 . . . . . . . . . . . . . . . . . . . . . . . 24
12522sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . 24
126124, 125sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . 23
12721, 126syl 16 . . . . . . . . . . . . . . . . . . . . . 22
128127adantr 465 . . . . . . . . . . . . . . . . . . . . 21
129123, 128syld 44 . . . . . . . . . . . . . . . . . . . 20
130129adantll 713 . . . . . . . . . . . . . . . . . . 19
131121, 130jcad 533 . . . . . . . . . . . . . . . . . 18
132 oveq2 6304 . . . . . . . . . . . . . . . . . . . 20
133132sseq2d 3531 . . . . . . . . . . . . . . . . . . 19
134133rspcev 3210 . . . . . . . . . . . . . . . . . 18
135131, 134syl6 33 . . . . . . . . . . . . . . . . 17
136135adantrr 716 . . . . . . . . . . . . . . . 16
137 omordi 7234 . . . . . . . . . . . . . . . . . . . . . . 23
13861, 137sylanl1 650 . . . . . . . . . . . . . . . . . . . . . 22
139138adantrd 468 . . . . . . . . . . . . . . . . . . . . 21
140139adantrr 716 . . . . . . . . . . . . . . . . . . . 20
141 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . 25
142141oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . 24
143 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . 25
144143oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . 24
145142, 144eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . . 23
146145rspccv 3207 . . . . . . . . . . . . . . . . . . . . . 22
147 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . 26
148 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
149147, 148syl5ib 219 . . . . . . . . . . . . . . . . . . . . . . . . 25
150 eqimss2 3556 . . . . . . . . . . . . . . . . . . . . . . . . 25
151149, 150syl6 33 . . . . . . . . . . . . . . . . . . . . . . . 24
152151imim2i 14 . . . . . . . . . . . . . . . . . . . . . . 23
153152impd 431 . . . . . . . . . . . . . . . . . . . . . 22
154146, 153syl 16 . . . . . . . . . . . . . . . . . . . . 21
155154ad2antll 728 . . . . . . . . . . . . . . . . . . . 20
156140, 155jcad 533 . . . . . . . . . . . . . . . . . . 19
157 oveq2 6304 . . . . . . . . . . . . . . . . . . . . 21
158157sseq2d 3531 . . . . . . . . . . . . . . . . . . . 20
159158rspcev 3210 . . . . . . . . . . . . . . . . . . 19
160156, 159syl6 33 . . . . . . . . . . . . . . . . . 18
161160rexlimdvw 2952 . . . . . . . . . . . . . . . . 17
162161adantlrr 720 . . . . . . . . . . . . . . . 16