Metamath Proof Explorer


Theorem oeoa

Description: Sum of exponents law for ordinal exponentiation. Theorem 8R of Enderton p. 238. Also Proposition 8.41 of TakeutiZaring p. 69. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoa AOnBOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C

Proof

Step Hyp Ref Expression
1 oa00 BOnCOnB+𝑜C=B=C=
2 1 biimpar BOnCOnB=C=B+𝑜C=
3 2 oveq2d BOnCOnB=C=𝑜B+𝑜C=𝑜
4 oveq2 B=𝑜B=𝑜
5 oveq2 C=𝑜C=𝑜
6 oe0m0 𝑜=1𝑜
7 5 6 eqtrdi C=𝑜C=1𝑜
8 4 7 oveqan12d B=C=𝑜B𝑜𝑜C=𝑜𝑜1𝑜
9 0elon On
10 oecl OnOn𝑜On
11 9 9 10 mp2an 𝑜On
12 om1 𝑜On𝑜𝑜1𝑜=𝑜
13 11 12 ax-mp 𝑜𝑜1𝑜=𝑜
14 8 13 eqtrdi B=C=𝑜B𝑜𝑜C=𝑜
15 14 adantl BOnCOnB=C=𝑜B𝑜𝑜C=𝑜
16 3 15 eqtr4d BOnCOnB=C=𝑜B+𝑜C=𝑜B𝑜𝑜C
17 oacl BOnCOnB+𝑜COn
18 on0eln0 B+𝑜COnB+𝑜CB+𝑜C
19 17 18 syl BOnCOnB+𝑜CB+𝑜C
20 oe0m1 B+𝑜COnB+𝑜C𝑜B+𝑜C=
21 17 20 syl BOnCOnB+𝑜C𝑜B+𝑜C=
22 1 necon3abid BOnCOnB+𝑜C¬B=C=
23 19 21 22 3bitr3d BOnCOn𝑜B+𝑜C=¬B=C=
24 23 biimpar BOnCOn¬B=C=𝑜B+𝑜C=
25 on0eln0 BOnBB
26 25 adantr BOnCOnBB
27 on0eln0 COnCC
28 27 adantl BOnCOnCC
29 26 28 orbi12d BOnCOnBCBC
30 neorian BC¬B=C=
31 29 30 bitrdi BOnCOnBC¬B=C=
32 oe0m1 BOnB𝑜B=
33 32 biimpa BOnB𝑜B=
34 33 oveq1d BOnB𝑜B𝑜𝑜C=𝑜𝑜C
35 oecl OnCOn𝑜COn
36 9 35 mpan COn𝑜COn
37 om0r 𝑜COn𝑜𝑜C=
38 36 37 syl COn𝑜𝑜C=
39 34 38 sylan9eq BOnBCOn𝑜B𝑜𝑜C=
40 39 an32s BOnCOnB𝑜B𝑜𝑜C=
41 oe0m1 COnC𝑜C=
42 41 biimpa COnC𝑜C=
43 42 oveq2d COnC𝑜B𝑜𝑜C=𝑜B𝑜
44 oecl OnBOn𝑜BOn
45 9 44 mpan BOn𝑜BOn
46 om0 𝑜BOn𝑜B𝑜=
47 45 46 syl BOn𝑜B𝑜=
48 43 47 sylan9eqr BOnCOnC𝑜B𝑜𝑜C=
49 48 anassrs BOnCOnC𝑜B𝑜𝑜C=
50 40 49 jaodan BOnCOnBC𝑜B𝑜𝑜C=
51 50 ex BOnCOnBC𝑜B𝑜𝑜C=
52 31 51 sylbird BOnCOn¬B=C=𝑜B𝑜𝑜C=
53 52 imp BOnCOn¬B=C=𝑜B𝑜𝑜C=
54 24 53 eqtr4d BOnCOn¬B=C=𝑜B+𝑜C=𝑜B𝑜𝑜C
55 16 54 pm2.61dan BOnCOn𝑜B+𝑜C=𝑜B𝑜𝑜C
56 oveq1 A=A𝑜B+𝑜C=𝑜B+𝑜C
57 oveq1 A=A𝑜B=𝑜B
58 oveq1 A=A𝑜C=𝑜C
59 57 58 oveq12d A=A𝑜B𝑜A𝑜C=𝑜B𝑜𝑜C
60 56 59 eqeq12d A=A𝑜B+𝑜C=A𝑜B𝑜A𝑜C𝑜B+𝑜C=𝑜B𝑜𝑜C
61 55 60 syl5ibr A=BOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C
62 61 impcom BOnCOnA=A𝑜B+𝑜C=A𝑜B𝑜A𝑜C
63 oveq1 A=ifAOnAA1𝑜A𝑜B+𝑜C=ifAOnAA1𝑜𝑜B+𝑜C
64 oveq1 A=ifAOnAA1𝑜A𝑜B=ifAOnAA1𝑜𝑜B
65 oveq1 A=ifAOnAA1𝑜A𝑜C=ifAOnAA1𝑜𝑜C
66 64 65 oveq12d A=ifAOnAA1𝑜A𝑜B𝑜A𝑜C=ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜C
67 63 66 eqeq12d A=ifAOnAA1𝑜A𝑜B+𝑜C=A𝑜B𝑜A𝑜CifAOnAA1𝑜𝑜B+𝑜C=ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜C
68 67 imbi2d A=ifAOnAA1𝑜COnA𝑜B+𝑜C=A𝑜B𝑜A𝑜CCOnifAOnAA1𝑜𝑜B+𝑜C=ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜C
69 oveq1 B=ifBOnB1𝑜B+𝑜C=ifBOnB1𝑜+𝑜C
70 69 oveq2d B=ifBOnB1𝑜ifAOnAA1𝑜𝑜B+𝑜C=ifAOnAA1𝑜𝑜ifBOnB1𝑜+𝑜C
71 oveq2 B=ifBOnB1𝑜ifAOnAA1𝑜𝑜B=ifAOnAA1𝑜𝑜ifBOnB1𝑜
72 71 oveq1d B=ifBOnB1𝑜ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜C=ifAOnAA1𝑜𝑜ifBOnB1𝑜𝑜ifAOnAA1𝑜𝑜C
73 70 72 eqeq12d B=ifBOnB1𝑜ifAOnAA1𝑜𝑜B+𝑜C=ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜CifAOnAA1𝑜𝑜ifBOnB1𝑜+𝑜C=ifAOnAA1𝑜𝑜ifBOnB1𝑜𝑜ifAOnAA1𝑜𝑜C
74 73 imbi2d B=ifBOnB1𝑜COnifAOnAA1𝑜𝑜B+𝑜C=ifAOnAA1𝑜𝑜B𝑜ifAOnAA1𝑜𝑜CCOnifAOnAA1𝑜𝑜ifBOnB1𝑜+𝑜C=ifAOnAA1𝑜𝑜ifBOnB1𝑜𝑜ifAOnAA1𝑜𝑜C
75 eleq1 A=ifAOnAA1𝑜AOnifAOnAA1𝑜On
76 eleq2 A=ifAOnAA1𝑜AifAOnAA1𝑜
77 75 76 anbi12d A=ifAOnAA1𝑜AOnAifAOnAA1𝑜OnifAOnAA1𝑜
78 eleq1 1𝑜=ifAOnAA1𝑜1𝑜OnifAOnAA1𝑜On
79 eleq2 1𝑜=ifAOnAA1𝑜1𝑜ifAOnAA1𝑜
80 78 79 anbi12d 1𝑜=ifAOnAA1𝑜1𝑜On1𝑜ifAOnAA1𝑜OnifAOnAA1𝑜
81 1on 1𝑜On
82 0lt1o 1𝑜
83 81 82 pm3.2i 1𝑜On1𝑜
84 77 80 83 elimhyp ifAOnAA1𝑜OnifAOnAA1𝑜
85 84 simpli ifAOnAA1𝑜On
86 84 simpri ifAOnAA1𝑜
87 81 elimel ifBOnB1𝑜On
88 85 86 87 oeoalem COnifAOnAA1𝑜𝑜ifBOnB1𝑜+𝑜C=ifAOnAA1𝑜𝑜ifBOnB1𝑜𝑜ifAOnAA1𝑜𝑜C
89 68 74 88 dedth2h AOnABOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C
90 89 impr AOnABOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C
91 90 an32s AOnBOnCOnAA𝑜B+𝑜C=A𝑜B𝑜A𝑜C
92 62 91 oe0lem AOnBOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C
93 92 3impb AOnBOnCOnA𝑜B+𝑜C=A𝑜B𝑜A𝑜C