Proof of Theorem relexpmulg
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. . . 4
⊢ (𝐽 ∈ ℕ0
↔ (𝐽 ∈ ℕ
∨ 𝐽 =
0)) |
| 2 | | elnn0 12528 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℕ
∨ 𝐾 =
0)) |
| 3 | | relexpmulnn 43722 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
| 4 | 3 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
| 5 | 4 | expcom 413 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
| 6 | 5 | expcom 413 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 7 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
| 8 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐾 = 0) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 𝐾) = (𝐽 · 0)) |
| 10 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℕ) |
| 11 | 10 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℂ) |
| 12 | 11 | mul01d 11460 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 0) = 0) |
| 13 | 7, 9, 12 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = 0) |
| 14 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐾 = 0 ∧ 𝐽 ∈ ℕ)) |
| 15 | | nnnle0 12299 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ ℕ → ¬
𝐽 ≤ 0) |
| 16 | 15 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 0) |
| 17 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → 𝐾 = 0) |
| 18 | 17 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝐽 ≤ 𝐾 ↔ 𝐽 ≤ 0)) |
| 19 | 16, 18 | mtbird 325 |
. . . . . . . . . . . . 13
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 𝐾) |
| 20 | 14, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ 𝐽 ≤ 𝐾) |
| 21 | 13, 20 | jcnd 163 |
. . . . . . . . . . 11
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ (𝐼 = 0 → 𝐽 ≤ 𝐾)) |
| 22 | 21 | pm2.21d 121 |
. . . . . . . . . 10
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
| 23 | 22 | exp32 420 |
. . . . . . . . 9
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝑅 ∈ 𝑉 → (𝐼 = (𝐽 · 𝐾) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))))) |
| 24 | 23 | 3impd 1349 |
. . . . . . . 8
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
| 25 | 24 | ex 412 |
. . . . . . 7
⊢ (𝐾 = 0 → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 26 | 6, 25 | jaoi 858 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ ∨ 𝐾 = 0) → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 27 | 2, 26 | sylbi 217 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈ ℕ
→ ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 28 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐽 = 0) |
| 29 | 28 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
| 30 | | simpr1 1195 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝑅 ∈ 𝑉) |
| 31 | | relexp0g 15061 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
| 33 | 29, 32 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾)) |
| 35 | | dmexg 7923 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
| 36 | | rnexg 7924 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
| 37 | 35, 36 | unexd 7774 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
| 38 | 30, 37 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
| 39 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈
ℕ0) |
| 40 | | relexpiidm 43717 |
. . . . . . . . 9
⊢ (((dom
𝑅 ∪ ran 𝑅) ∈ V ∧ 𝐾 ∈ ℕ0)
→ (( I ↾ (dom 𝑅
∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
| 41 | 38, 39, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
| 42 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
| 43 | 28 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝐽 · 𝐾) = (0 · 𝐾)) |
| 44 | 39 | nn0cnd 12589 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈ ℂ) |
| 45 | 44 | mul02d 11459 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (0 · 𝐾) = 0) |
| 46 | 42, 43, 45 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = 0) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
| 48 | 47, 32 | eqtr2d 2778 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝐼)) |
| 49 | 34, 41, 48 | 3eqtrd 2781 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
| 50 | 49 | ex 412 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
| 51 | 50 | ex 412 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 = 0 →
((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 52 | 27, 51 | jaod 860 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ ((𝐽 ∈ ℕ
∨ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 53 | 1, 52 | biimtrid 242 |
. . 3
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈
ℕ0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
| 54 | 53 | impcom 407 |
. 2
⊢ ((𝐽 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
| 55 | 54 | impcom 407 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0))
→ ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |