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. Theorem 4.7 of Schloeder p. 14. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Assertion oeoa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C

Proof

Step Hyp Ref Expression
1 oa00 ⊢ B ∈ On ∧ C ∈ On → B + 𝑜 C = ∅ ↔ B = ∅ ∧ C = ∅
2 1 biimpar ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∧ C = ∅ → B + 𝑜 C = ∅
3 2 oveq2d ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∧ 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 ⊢ ∅ ∈ On ∧ ∅ ∈ On → ∅ ↑ 𝑜 ∅ ∈ 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 ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅ ↑ 𝑜 ∅
16 3 15 eqtr4d ⊢ B ∈ On ∧ C ∈ On ∧ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B + 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C
17 oacl ⊢ B ∈ On ∧ C ∈ On → B + 𝑜 C ∈ On
18 on0eln0 ⊢ B + 𝑜 C ∈ On → ∅ ∈ B + 𝑜 C ↔ B + 𝑜 C ≠ ∅
19 17 18 syl ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B + 𝑜 C ↔ B + 𝑜 C ≠ ∅
20 oe0m1 ⊢ B + 𝑜 C ∈ On → ∅ ∈ B + 𝑜 C ↔ ∅ ↑ 𝑜 B + 𝑜 C = ∅
21 17 20 syl ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B + 𝑜 C ↔ ∅ ↑ 𝑜 B + 𝑜 C = ∅
22 1 necon3abid ⊢ B ∈ On ∧ C ∈ On → B + 𝑜 C ≠ ∅ ↔ ¬ B = ∅ ∧ C = ∅
23 19 21 22 3bitr3d ⊢ B ∈ On ∧ C ∈ On → ∅ ↑ 𝑜 B + 𝑜 C = ∅ ↔ ¬ B = ∅ ∧ C = ∅
24 23 biimpar ⊢ B ∈ On ∧ C ∈ On ∧ ¬ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B + 𝑜 C = ∅
25 on0eln0 ⊢ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
26 25 adantr ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ↔ B ≠ ∅
27 on0eln0 ⊢ C ∈ On → ∅ ∈ C ↔ C ≠ ∅
28 27 adantl ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ C ↔ C ≠ ∅
29 26 28 orbi12d ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∨ ∅ ∈ C ↔ B ≠ ∅ ∨ C ≠ ∅
30 neorian ⊢ B ≠ ∅ ∨ C ≠ ∅ ↔ ¬ B = ∅ ∧ C = ∅
31 29 30 bitrdi ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∨ ∅ ∈ C ↔ ¬ B = ∅ ∧ C = ∅
32 oe0m1 ⊢ B ∈ On → ∅ ∈ B ↔ ∅ ↑ 𝑜 B = ∅
33 32 biimpa ⊢ B ∈ On ∧ ∅ ∈ B → ∅ ↑ 𝑜 B = ∅
34 33 oveq1d ⊢ B ∈ On ∧ ∅ ∈ B → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅ ⋅ 𝑜 ∅ ↑ 𝑜 C
35 oecl ⊢ ∅ ∈ On ∧ C ∈ On → ∅ ↑ 𝑜 C ∈ On
36 9 35 mpan ⊢ C ∈ On → ∅ ↑ 𝑜 C ∈ On
37 om0r ⊢ ∅ ↑ 𝑜 C ∈ On → ∅ ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
38 36 37 syl ⊢ C ∈ On → ∅ ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
39 34 38 sylan9eq ⊢ B ∈ On ∧ ∅ ∈ B ∧ C ∈ On → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
40 39 an32s ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
41 oe0m1 ⊢ C ∈ On → ∅ ∈ C ↔ ∅ ↑ 𝑜 C = ∅
42 41 biimpa ⊢ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 C = ∅
43 42 oveq2d ⊢ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 ∅
44 oecl ⊢ ∅ ∈ On ∧ B ∈ On → ∅ ↑ 𝑜 B ∈ On
45 9 44 mpan ⊢ B ∈ On → ∅ ↑ 𝑜 B ∈ On
46 om0 ⊢ ∅ ↑ 𝑜 B ∈ On → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ = ∅
47 45 46 syl ⊢ B ∈ On → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ = ∅
48 43 47 sylan9eqr ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
49 48 anassrs ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
50 40 49 jaodan ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B ∨ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
51 50 ex ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ∨ ∅ ∈ C → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
52 31 51 sylbird ⊢ B ∈ On ∧ C ∈ On → ¬ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
53 52 imp ⊢ B ∈ On ∧ C ∈ On ∧ ¬ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C = ∅
54 24 53 eqtr4d ⊢ B ∈ On ∧ C ∈ On ∧ ¬ B = ∅ ∧ C = ∅ → ∅ ↑ 𝑜 B + 𝑜 C = ∅ ↑ 𝑜 B ⋅ 𝑜 ∅ ↑ 𝑜 C
55 16 54 pm2.61dan ⊢ B ∈ On ∧ C ∈ On → ∅ ↑ 𝑜 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 imbitrrid ⊢ A = ∅ → B ∈ On ∧ C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
62 61 impcom ⊢ B ∈ On ∧ C ∈ On ∧ A = ∅ → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
63 oveq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C
64 oveq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B
65 oveq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
66 64 65 oveq12d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
67 63 66 eqeq12d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
68 67 imbi2d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C ↔ C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
69 oveq1 ⊢ B = if B ∈ On B 1 𝑜 → B + 𝑜 C = if B ∈ On B 1 𝑜 + 𝑜 C
70 69 oveq2d ⊢ B = if B ∈ On B 1 𝑜 → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 + 𝑜 C
71 oveq2 ⊢ B = if B ∈ On B 1 𝑜 → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜
72 71 oveq1d ⊢ B = if B ∈ On B 1 𝑜 → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
73 70 72 eqeq12d ⊢ B = if B ∈ On B 1 𝑜 → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
74 73 imbi2d ⊢ B = if B ∈ On B 1 𝑜 → C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 B ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C ↔ C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
75 eleq1 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ∈ On ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
76 eleq2 ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → ∅ ∈ A ↔ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
77 75 76 anbi12d ⊢ A = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → A ∈ On ∧ ∅ ∈ A ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
78 eleq1 ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → 1 𝑜 ∈ On ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
79 eleq2 ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → ∅ ∈ 1 𝑜 ↔ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
80 78 79 anbi12d ⊢ 1 𝑜 = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 → 1 𝑜 ∈ On ∧ ∅ ∈ 1 𝑜 ↔ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
81 1on ⊢ 1 𝑜 ∈ On
82 0lt1o ⊢ ∅ ∈ 1 𝑜
83 81 82 pm3.2i ⊢ 1 𝑜 ∈ On ∧ ∅ ∈ 1 𝑜
84 77 80 83 elimhyp ⊢ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On ∧ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
85 84 simpli ⊢ if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ∈ On
86 84 simpri ⊢ ∅ ∈ if A ∈ On ∧ ∅ ∈ A A 1 𝑜
87 81 elimel ⊢ if B ∈ On B 1 𝑜 ∈ On
88 85 86 87 oeoalem ⊢ C ∈ On → if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 + 𝑜 C = if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 if B ∈ On B 1 𝑜 ⋅ 𝑜 if A ∈ On ∧ ∅ ∈ A A 1 𝑜 ↑ 𝑜 C
89 68 74 88 dedth2h ⊢ A ∈ On ∧ ∅ ∈ A ∧ B ∈ On → C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
90 89 impr ⊢ A ∈ On ∧ ∅ ∈ A ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
91 90 an32s ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ A → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
92 62 91 oe0lem ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C
93 92 3impb ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B + 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 A ↑ 𝑜 C