Proof of Theorem relexpmulg
Step | Hyp | Ref
| Expression |
1 | | elnn0 12121 |
. . . 4
⊢ (𝐽 ∈ ℕ0
↔ (𝐽 ∈ ℕ
∨ 𝐽 =
0)) |
2 | | elnn0 12121 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℕ
∨ 𝐾 =
0)) |
3 | | relexpmulnn 41041 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
4 | 3 | 3adantl3 1170 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
5 | 4 | expcom 417 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
6 | 5 | expcom 417 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
7 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
8 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐾 = 0) |
9 | 8 | oveq2d 7250 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 𝐾) = (𝐽 · 0)) |
10 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℕ) |
11 | 10 | nncnd 11875 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℂ) |
12 | 11 | mul01d 11060 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 0) = 0) |
13 | 7, 9, 12 | 3eqtrd 2783 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = 0) |
14 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐾 = 0 ∧ 𝐽 ∈ ℕ)) |
15 | | nnnle0 11892 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ ℕ → ¬
𝐽 ≤ 0) |
16 | 15 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 0) |
17 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → 𝐾 = 0) |
18 | 17 | breq2d 5081 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝐽 ≤ 𝐾 ↔ 𝐽 ≤ 0)) |
19 | 16, 18 | mtbird 328 |
. . . . . . . . . . . . 13
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 𝐾) |
20 | 14, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ 𝐽 ≤ 𝐾) |
21 | 13, 20 | jcnd 166 |
. . . . . . . . . . 11
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ (𝐼 = 0 → 𝐽 ≤ 𝐾)) |
22 | 21 | pm2.21d 121 |
. . . . . . . . . 10
⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
23 | 22 | exp32 424 |
. . . . . . . . 9
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝑅 ∈ 𝑉 → (𝐼 = (𝐽 · 𝐾) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))))) |
24 | 23 | 3impd 1350 |
. . . . . . . 8
⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
25 | 24 | ex 416 |
. . . . . . 7
⊢ (𝐾 = 0 → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
26 | 6, 25 | jaoi 857 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ ∨ 𝐾 = 0) → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
27 | 2, 26 | sylbi 220 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈ ℕ
→ ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
28 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐽 = 0) |
29 | 28 | oveq2d 7250 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = (𝑅↑𝑟0)) |
30 | | simpr1 1196 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝑅 ∈ 𝑉) |
31 | | relexp0g 14617 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) |
33 | 29, 32 | eqtrd 2779 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
34 | 33 | oveq1d 7249 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾)) |
35 | | dmexg 7702 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
36 | | rnexg 7703 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
37 | | unexg 7555 |
. . . . . . . . . . 11
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
39 | 30, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
40 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈
ℕ0) |
41 | | relexpiidm 41036 |
. . . . . . . . 9
⊢ (((dom
𝑅 ∪ ran 𝑅) ∈ V ∧ 𝐾 ∈ ℕ0)
→ (( I ↾ (dom 𝑅
∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
42 | 39, 40, 41 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) |
43 | | simpr2 1197 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = (𝐽 · 𝐾)) |
44 | 28 | oveq1d 7249 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝐽 · 𝐾) = (0 · 𝐾)) |
45 | 40 | nn0cnd 12181 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈ ℂ) |
46 | 45 | mul02d 11059 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (0 · 𝐾) = 0) |
47 | 43, 44, 46 | 3eqtrd 2783 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = 0) |
48 | 47 | oveq2d 7250 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑𝑟𝐼) = (𝑅↑𝑟0)) |
49 | 48, 32 | eqtr2d 2780 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝐼)) |
50 | 34, 42, 49 | 3eqtrd 2783 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |
51 | 50 | ex 416 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
52 | 51 | ex 416 |
. . . . 5
⊢ (𝐾 ∈ ℕ0
→ (𝐽 = 0 →
((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
53 | 27, 52 | jaod 859 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ ((𝐽 ∈ ℕ
∨ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
54 | 1, 53 | syl5bi 245 |
. . 3
⊢ (𝐾 ∈ ℕ0
→ (𝐽 ∈
ℕ0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)))) |
55 | 54 | impcom 411 |
. 2
⊢ ((𝐽 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼))) |
56 | 55 | impcom 411 |
1
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0))
→ ((𝑅↑𝑟𝐽)↑𝑟𝐾) = (𝑅↑𝑟𝐼)) |