Proof of Theorem relexpmulg
Step | Hyp | Ref
| Expression |
1 | | elnn0 11294 |
. . . 4
⊢ (𝐽 ∈ ℕ0
↔ (𝐽 ∈ ℕ
∨ 𝐽 =
0)) |
2 | | elnn0 11294 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℕ
∨ 𝐾 =
0)) |
3 | | relexpmulnn 38001 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
4 | 3 | 3adantl3 1219 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
5 | 4 | expcom 451 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
6 | 5 | expcom 451 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
7 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
8 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐾 = 0) |
9 | 8 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 𝐾) = (𝐽 · 0)) |
10 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℕ) |
11 | 10 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℂ) |
12 | 11 | mul01d 10235 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 0) = 0) |
13 | 7, 9, 12 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = 0) |
14 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐾 = 0 ∧ 𝐽 ∈ ℕ)) |
15 | | nnnle0 11051 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ ℕ → ¬
𝐽 ≤ 0) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 0) |
17 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → 𝐾 = 0) |
18 | 17 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝐽 ≤ 𝐾 ↔ 𝐽 ≤ 0)) |
19 | 16, 18 | mtbird 315 |
. . . . . . . . . . . . 13
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 𝐾) |
20 | 14, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ 𝐽 ≤ 𝐾) |
21 | | mth8 158 |
. . . . . . . . . . . 12
⊢ (𝐼 = 0 → (¬ 𝐽 ≤ 𝐾 → ¬ (𝐼 = 0 → 𝐽 ≤ 𝐾))) |
22 | 13, 20, 21 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ (𝐼 = 0 → 𝐽 ≤ 𝐾)) |
23 | 22 | pm2.21d 118 |
. . . . . . . . . 10
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
24 | 23 | exp32 631 |
. . . . . . . . 9
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝑅 ∈ 𝑉 → (𝐼 = (𝐽 · 𝐾) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))))) |
25 | 24 | 3impd 1281 |
. . . . . . . 8
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
26 | 25 | ex 450 |
. . . . . . 7
⊢ (𝐾 = 0 → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
27 | 6, 26 | jaoi 394 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ ∨ 𝐾 = 0) → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
28 | 2, 27 | sylbi 207 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈ ℕ
→ ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
29 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐽 = 0) |
30 | 29 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
31 | | simpr1 1067 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝑅 ∈ 𝑉) |
32 | | relexp0g 13762 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
34 | 30, 33 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
35 | 34 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾)) |
36 | | dmexg 7097 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
37 | | rnexg 7098 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
38 | | unexg 6959 |
. . . . . . . . . . 11
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
39 | 36, 37, 38 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
40 | 31, 39 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
41 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈
ℕ0) |
42 | | relexpiidm 37996 |
. . . . . . . . 9
⊢ (((dom
𝑅 ∪ ran 𝑅) ∈ V ∧ 𝐾 ∈ ℕ0)
→ (( I ↾ (dom 𝑅
∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
44 | | simpr2 1068 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
45 | 29 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝐽 · 𝐾) = (0 · 𝐾)) |
46 | 41 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈ ℂ) |
47 | 46 | mul02d 10234 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (0 · 𝐾) = 0) |
48 | 44, 45, 47 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = 0) |
49 | 48 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
50 | 49, 33 | eqtr2d 2657 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝐼)) |
51 | 35, 43, 50 | 3eqtrd 2660 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
52 | 51 | ex 450 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
53 | 52 | ex 450 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 = 0 →
((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
54 | 28, 53 | jaod 395 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ ((𝐽 ∈ ℕ
∨ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
55 | 1, 54 | syl5bi 232 |
. . 3
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈
ℕ0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
56 | 55 | impcom 446 |
. 2
⊢ ((𝐽 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
57 | 56 | impcom 446 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0))
→ ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |