Proof of Theorem relexpaddg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elnn0 12528 | . . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) | 
| 2 |  | elnn0 12528 | . . . . . . 7
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) | 
| 3 |  | relexpaddnn 15090 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 4 | 3 | a1d 25 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 5 | 4 | 3exp 1120 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ ℕ → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 6 | 5 | com12 32 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 7 |  | elnn1uz2 12967 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) | 
| 8 |  | coires1 6284 | . . . . . . . . . . . . . 14
⊢ ((𝑅↑𝑟𝑁) ∘ ( I ↾ (dom 𝑅 ∪ ran 𝑅))) = ((𝑅↑𝑟𝑁) ↾ (dom 𝑅 ∪ ran 𝑅)) | 
| 9 |  | simpll 767 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑁 = 1) | 
| 10 |  | simplr 769 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑀 = 0) | 
| 11 | 9, 10 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = (1 + 0)) | 
| 12 |  | 1p0e1 12390 | . . . . . . . . . . . . . . . . . 18
⊢ (1 + 0) =
1 | 
| 13 | 11, 12 | eqtrdi 2793 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = 1) | 
| 14 |  | simprr 773 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑁 + 𝑀) = 1 → Rel 𝑅)) | 
| 15 | 13, 14 | mpd 15 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → Rel 𝑅) | 
| 16 | 9 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟1)) | 
| 17 |  | simprl 771 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑅 ∈ 𝑉) | 
| 18 |  | relexp1g 15065 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟1) = 𝑅) | 
| 20 | 16, 19 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟𝑁) = 𝑅) | 
| 21 | 20 | releqd 5788 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (Rel (𝑅↑𝑟𝑁) ↔ Rel 𝑅)) | 
| 22 | 15, 21 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → Rel (𝑅↑𝑟𝑁)) | 
| 23 |  | 1nn 12277 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ | 
| 24 | 9, 23 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑁 ∈ ℕ) | 
| 25 |  | relexpnndm 15080 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅) | 
| 26 | 24, 17, 25 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅) | 
| 27 |  | ssun1 4178 | . . . . . . . . . . . . . . . 16
⊢ dom 𝑅 ⊆ (dom 𝑅 ∪ ran 𝑅) | 
| 28 | 26, 27 | sstrdi 3996 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) | 
| 29 |  | relssres 6040 | . . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑅↑𝑟𝑁) ∧ dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) → ((𝑅↑𝑟𝑁) ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝑁)) | 
| 30 | 22, 28, 29 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝑁)) | 
| 31 | 8, 30 | eqtrid 2789 | . . . . . . . . . . . . 13
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ ( I ↾ (dom 𝑅 ∪ ran 𝑅))) = (𝑅↑𝑟𝑁)) | 
| 32 | 10 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟𝑀) = (𝑅↑𝑟0)) | 
| 33 |  | relexp0g 15061 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) | 
| 34 | 17, 33 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) | 
| 35 | 32, 34 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟𝑀) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 36 | 35 | coeq2d 5873 | . . . . . . . . . . . . 13
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ((𝑅↑𝑟𝑁) ∘ ( I ↾ (dom 𝑅 ∪ ran 𝑅)))) | 
| 37 | 10 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = (𝑁 + 0)) | 
| 38 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ | 
| 39 | 9, 38 | eqeltrdi 2849 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑁 ∈ ℂ) | 
| 40 | 39 | addridd 11461 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 0) = 𝑁) | 
| 41 | 37, 40 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = 𝑁) | 
| 42 | 41 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟(𝑁 + 𝑀)) = (𝑅↑𝑟𝑁)) | 
| 43 | 31, 36, 42 | 3eqtr4d 2787 | . . . . . . . . . . . 12
⊢ (((𝑁 = 1 ∧ 𝑀 = 0) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 44 | 43 | exp43 436 | . . . . . . . . . . 11
⊢ (𝑁 = 1 → (𝑀 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 45 |  | simp1 1137 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈
(ℤ≥‘2)) | 
| 46 |  | simp3 1139 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) | 
| 47 |  | relexpuzrel 15091 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟𝑁)) | 
| 48 | 45, 46, 47 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟𝑁)) | 
| 49 |  | eluz2nn 12924 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) | 
| 50 | 45, 49 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ ℕ) | 
| 51 | 50, 46, 25 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ dom 𝑅) | 
| 52 | 51, 27 | sstrdi 3996 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟𝑁) ⊆ (dom 𝑅 ∪ ran 𝑅)) | 
| 53 | 48, 52, 29 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟𝑁)) | 
| 54 | 8, 53 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ ( I ↾ (dom 𝑅 ∪ ran 𝑅))) = (𝑅↑𝑟𝑁)) | 
| 55 |  | simp2 1138 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑀 = 0) | 
| 56 | 55 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑀) = (𝑅↑𝑟0)) | 
| 57 | 46, 33 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) | 
| 58 | 56, 57 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑀) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 59 | 58 | coeq2d 5873 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ((𝑅↑𝑟𝑁) ∘ ( I ↾ (dom 𝑅 ∪ ran 𝑅)))) | 
| 60 | 55 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = (𝑁 + 0)) | 
| 61 |  | eluzelcn 12890 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) | 
| 62 | 45, 61 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ ℂ) | 
| 63 | 62 | addridd 11461 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑁 + 0) = 𝑁) | 
| 64 | 60, 63 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = 𝑁) | 
| 65 | 64 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟(𝑁 + 𝑀)) = (𝑅↑𝑟𝑁)) | 
| 66 | 54, 59, 65 | 3eqtr4d 2787 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 67 | 66 | a1d 25 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 68 | 67 | 3exp 1120 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑀 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 69 | 44, 68 | jaoi 858 | . . . . . . . . . 10
⊢ ((𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2))
→ (𝑀 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 70 | 7, 69 | sylbi 217 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑀 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 71 | 70 | com12 32 | . . . . . . . 8
⊢ (𝑀 = 0 → (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 72 | 6, 71 | jaoi 858 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → (𝑁 ∈ ℕ → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 73 | 2, 72 | sylbi 217 | . . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈ ℕ
→ (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 74 | 73 | com12 32 | . . . . 5
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ ℕ0
→ (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 75 | 74 | 3impd 1349 | . . . 4
⊢ (𝑁 ∈ ℕ → ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅)) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 76 |  | elnn1uz2 12967 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ ↔ (𝑀 = 1 ∨ 𝑀 ∈
(ℤ≥‘2))) | 
| 77 |  | coires1 6284 | . . . . . . . . . . . . . . 15
⊢ (◡𝑅 ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) = (◡𝑅 ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) | 
| 78 |  | relcnv 6122 | . . . . . . . . . . . . . . . . 17
⊢ Rel ◡𝑅 | 
| 79 |  | ssun1 4178 | . . . . . . . . . . . . . . . . 17
⊢ dom ◡𝑅 ⊆ (dom ◡𝑅 ∪ ran ◡𝑅) | 
| 80 | 78, 79 | pm3.2i 470 | . . . . . . . . . . . . . . . 16
⊢ (Rel
◡𝑅 ∧ dom ◡𝑅 ⊆ (dom ◡𝑅 ∪ ran ◡𝑅)) | 
| 81 |  | relssres 6040 | . . . . . . . . . . . . . . . 16
⊢ ((Rel
◡𝑅 ∧ dom ◡𝑅 ⊆ (dom ◡𝑅 ∪ ran ◡𝑅)) → (◡𝑅 ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) = ◡𝑅) | 
| 82 | 80, 81 | mp1i 13 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅 ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) = ◡𝑅) | 
| 83 | 77, 82 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅 ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) = ◡𝑅) | 
| 84 |  | cnvco 5896 | . . . . . . . . . . . . . . 15
⊢ ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (◡(𝑅↑𝑟𝑀) ∘ ◡(𝑅↑𝑟𝑁)) | 
| 85 |  | simplr 769 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑀 = 1) | 
| 86 |  | 1nn0 12542 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ0 | 
| 87 | 85, 86 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑀 ∈
ℕ0) | 
| 88 |  | simprl 771 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑅 ∈ 𝑉) | 
| 89 |  | relexpcnv 15074 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑀) = (◡𝑅↑𝑟𝑀)) | 
| 90 | 87, 88, 89 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟𝑀) = (◡𝑅↑𝑟𝑀)) | 
| 91 | 85 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅↑𝑟𝑀) = (◡𝑅↑𝑟1)) | 
| 92 |  | cnvexg 7946 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ 𝑉 → ◡𝑅 ∈ V) | 
| 93 | 88, 92 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡𝑅 ∈ V) | 
| 94 |  | relexp1g 15065 | . . . . . . . . . . . . . . . . . 18
⊢ (◡𝑅 ∈ V → (◡𝑅↑𝑟1) = ◡𝑅) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅↑𝑟1) = ◡𝑅) | 
| 96 | 90, 91, 95 | 3eqtrd 2781 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟𝑀) = ◡𝑅) | 
| 97 |  | simpll 767 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑁 = 0) | 
| 98 |  | 0nn0 12541 | . . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℕ0 | 
| 99 | 97, 98 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → 𝑁 ∈
ℕ0) | 
| 100 |  | relexpcnv 15074 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | 
| 101 | 99, 88, 100 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | 
| 102 | 97 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅↑𝑟𝑁) = (◡𝑅↑𝑟0)) | 
| 103 |  | relexp0g 15061 | . . . . . . . . . . . . . . . . . 18
⊢ (◡𝑅 ∈ V → (◡𝑅↑𝑟0) = ( I ↾
(dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 104 | 93, 103 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅↑𝑟0) = ( I ↾
(dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 105 | 101, 102,
104 | 3eqtrd 2781 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟𝑁) = ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 106 | 96, 105 | coeq12d 5875 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡(𝑅↑𝑟𝑀) ∘ ◡(𝑅↑𝑟𝑁)) = (◡𝑅 ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅)))) | 
| 107 | 84, 106 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (◡𝑅 ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅)))) | 
| 108 | 99, 87 | nn0addcld 12591 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) ∈
ℕ0) | 
| 109 |  | relexpcnv 15074 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 + 𝑀) ∈ ℕ0 ∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟(𝑁 + 𝑀)) = (◡𝑅↑𝑟(𝑁 + 𝑀))) | 
| 110 | 108, 88, 109 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟(𝑁 + 𝑀)) = (◡𝑅↑𝑟(𝑁 + 𝑀))) | 
| 111 | 97, 85 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = (0 + 1)) | 
| 112 |  | 0p1e1 12388 | . . . . . . . . . . . . . . . . 17
⊢ (0 + 1) =
1 | 
| 113 | 111, 112 | eqtrdi 2793 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑁 + 𝑀) = 1) | 
| 114 | 113 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (◡𝑅↑𝑟(𝑁 + 𝑀)) = (◡𝑅↑𝑟1)) | 
| 115 | 110, 114,
95 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡(𝑅↑𝑟(𝑁 + 𝑀)) = ◡𝑅) | 
| 116 | 83, 107, 115 | 3eqtr4d 2787 | . . . . . . . . . . . . 13
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ◡(𝑅↑𝑟(𝑁 + 𝑀))) | 
| 117 |  | relco 6126 | . . . . . . . . . . . . . 14
⊢ Rel
((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) | 
| 118 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑁 + 𝑀) = 1 → Rel 𝑅)) | 
| 119 | 113, 118 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → Rel 𝑅) | 
| 120 | 113 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟(𝑁 + 𝑀)) = (𝑅↑𝑟1)) | 
| 121 | 88, 18 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟1) = 𝑅) | 
| 122 | 120, 121 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (𝑅↑𝑟(𝑁 + 𝑀)) = 𝑅) | 
| 123 | 122 | releqd 5788 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (Rel (𝑅↑𝑟(𝑁 + 𝑀)) ↔ Rel 𝑅)) | 
| 124 | 119, 123 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → Rel (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 125 |  | cnveqb 6216 | . . . . . . . . . . . . . 14
⊢ ((Rel
((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) ∧ Rel (𝑅↑𝑟(𝑁 + 𝑀))) → (((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)) ↔ ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ◡(𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 126 | 117, 124,
125 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → (((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)) ↔ ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ◡(𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 127 | 116, 126 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝑁 = 0 ∧ 𝑀 = 1) ∧ (𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 128 | 127 | exp43 436 | . . . . . . . . . . 11
⊢ (𝑁 = 0 → (𝑀 = 1 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 129 | 128 | com12 32 | . . . . . . . . . 10
⊢ (𝑀 = 1 → (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 130 |  | coires1 6284 | . . . . . . . . . . . . . . . . 17
⊢ ((◡𝑅↑𝑟𝑀) ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) = ((◡𝑅↑𝑟𝑀) ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) | 
| 131 |  | simp2 1138 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑀 ∈
(ℤ≥‘2)) | 
| 132 |  | simp3 1139 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) | 
| 133 | 132, 92 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡𝑅 ∈ V) | 
| 134 |  | relexpuzrel 15091 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈
(ℤ≥‘2) ∧ ◡𝑅 ∈ V) → Rel (◡𝑅↑𝑟𝑀)) | 
| 135 | 131, 133,
134 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → Rel (◡𝑅↑𝑟𝑀)) | 
| 136 |  | eluz2nn 12924 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℕ) | 
| 137 | 131, 136 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑀 ∈ ℕ) | 
| 138 |  | relexpnndm 15080 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ ∧ ◡𝑅 ∈ V) → dom (◡𝑅↑𝑟𝑀) ⊆ dom ◡𝑅) | 
| 139 | 137, 133,
138 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → dom (◡𝑅↑𝑟𝑀) ⊆ dom ◡𝑅) | 
| 140 | 139, 79 | sstrdi 3996 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → dom (◡𝑅↑𝑟𝑀) ⊆ (dom ◡𝑅 ∪ ran ◡𝑅)) | 
| 141 |  | relssres 6040 | . . . . . . . . . . . . . . . . . 18
⊢ ((Rel
(◡𝑅↑𝑟𝑀) ∧ dom (◡𝑅↑𝑟𝑀) ⊆ (dom ◡𝑅 ∪ ran ◡𝑅)) → ((◡𝑅↑𝑟𝑀) ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) = (◡𝑅↑𝑟𝑀)) | 
| 142 | 135, 140,
141 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ((◡𝑅↑𝑟𝑀) ↾ (dom ◡𝑅 ∪ ran ◡𝑅)) = (◡𝑅↑𝑟𝑀)) | 
| 143 | 130, 142 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ((◡𝑅↑𝑟𝑀) ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) = (◡𝑅↑𝑟𝑀)) | 
| 144 |  | simp1 1137 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑁 = 0) | 
| 145 | 144 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟𝑁) = (◡𝑅↑𝑟0)) | 
| 146 | 133, 103 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟0) = ( I ↾
(dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 147 | 145, 146 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟𝑁) = ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅))) | 
| 148 | 147 | coeq2d 5873 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ((◡𝑅↑𝑟𝑀) ∘ (◡𝑅↑𝑟𝑁)) = ((◡𝑅↑𝑟𝑀) ∘ ( I ↾ (dom ◡𝑅 ∪ ran ◡𝑅)))) | 
| 149 | 144 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = (0 + 𝑀)) | 
| 150 |  | eluzelcn 12890 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℂ) | 
| 151 | 131, 150 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑀 ∈ ℂ) | 
| 152 | 151 | addlidd 11462 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (0 + 𝑀) = 𝑀) | 
| 153 | 149, 152 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = 𝑀) | 
| 154 | 153 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (◡𝑅↑𝑟(𝑁 + 𝑀)) = (◡𝑅↑𝑟𝑀)) | 
| 155 | 143, 148,
154 | 3eqtr4d 2787 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ((◡𝑅↑𝑟𝑀) ∘ (◡𝑅↑𝑟𝑁)) = (◡𝑅↑𝑟(𝑁 + 𝑀))) | 
| 156 |  | nnnn0 12533 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 157 | 131, 136,
156 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑀 ∈
ℕ0) | 
| 158 | 157, 132,
89 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑀) = (◡𝑅↑𝑟𝑀)) | 
| 159 | 144, 98 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑁 ∈
ℕ0) | 
| 160 | 159, 132,
100 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟𝑁) = (◡𝑅↑𝑟𝑁)) | 
| 161 | 158, 160 | coeq12d 5875 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (◡(𝑅↑𝑟𝑀) ∘ ◡(𝑅↑𝑟𝑁)) = ((◡𝑅↑𝑟𝑀) ∘ (◡𝑅↑𝑟𝑁))) | 
| 162 | 84, 161 | eqtrid 2789 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ((◡𝑅↑𝑟𝑀) ∘ (◡𝑅↑𝑟𝑁))) | 
| 163 | 159, 157 | nn0addcld 12591 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) ∈
ℕ0) | 
| 164 | 163, 132,
109 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡(𝑅↑𝑟(𝑁 + 𝑀)) = (◡𝑅↑𝑟(𝑁 + 𝑀))) | 
| 165 | 155, 162,
164 | 3eqtr4d 2787 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ◡(𝑅↑𝑟(𝑁 + 𝑀))) | 
| 166 | 159 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ ℂ) | 
| 167 | 151, 166 | addcomd 11463 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑀 + 𝑁) = (𝑁 + 𝑀)) | 
| 168 |  | uzaddcl 12946 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈
(ℤ≥‘2)) | 
| 169 | 131, 159,
168 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑀 + 𝑁) ∈
(ℤ≥‘2)) | 
| 170 | 167, 169 | eqeltrrd 2842 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) ∈
(ℤ≥‘2)) | 
| 171 |  | relexpuzrel 15091 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 + 𝑀) ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 172 | 170, 132,
171 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 173 | 117, 172,
125 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)) ↔ ◡((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ◡(𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 174 | 165, 173 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 175 | 174 | a1d 25 | . . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑀 ∈ (ℤ≥‘2)
∧ 𝑅 ∈ 𝑉) → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 176 | 175 | 3exp 1120 | . . . . . . . . . . 11
⊢ (𝑁 = 0 → (𝑀 ∈ (ℤ≥‘2)
→ (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 177 | 176 | com12 32 | . . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘2) → (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 178 | 129, 177 | jaoi 858 | . . . . . . . . 9
⊢ ((𝑀 = 1 ∨ 𝑀 ∈ (ℤ≥‘2))
→ (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 179 | 76, 178 | sylbi 217 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 180 |  | coires1 6284 | . . . . . . . . . . . . 13
⊢ ((𝑅↑𝑟0)
∘ ( I ↾ (dom 𝑅
∪ ran 𝑅))) = ((𝑅↑𝑟0)
↾ (dom 𝑅 ∪ ran
𝑅)) | 
| 181 |  | simp3 1139 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ 𝑉) | 
| 182 |  | relexp0rel 15076 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ 𝑉 → Rel (𝑅↑𝑟0)) | 
| 183 | 181, 182 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → Rel (𝑅↑𝑟0)) | 
| 184 | 181, 33 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟0) = ( I ↾
(dom 𝑅 ∪ ran 𝑅))) | 
| 185 | 184 | dmeqd 5916 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟0) = dom ( I
↾ (dom 𝑅 ∪ ran
𝑅))) | 
| 186 |  | dmresi 6070 | . . . . . . . . . . . . . . . 16
⊢ dom ( I
↾ (dom 𝑅 ∪ ran
𝑅)) = (dom 𝑅 ∪ ran 𝑅) | 
| 187 | 185, 186 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟0) = (dom 𝑅 ∪ ran 𝑅)) | 
| 188 |  | eqimss 4042 | . . . . . . . . . . . . . . 15
⊢ (dom
(𝑅↑𝑟0) = (dom 𝑅 ∪ ran 𝑅) → dom (𝑅↑𝑟0) ⊆ (dom
𝑅 ∪ ran 𝑅)) | 
| 189 | 187, 188 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → dom (𝑅↑𝑟0) ⊆ (dom
𝑅 ∪ ran 𝑅)) | 
| 190 |  | relssres 6040 | . . . . . . . . . . . . . 14
⊢ ((Rel
(𝑅↑𝑟0) ∧ dom
(𝑅↑𝑟0) ⊆ (dom
𝑅 ∪ ran 𝑅)) → ((𝑅↑𝑟0) ↾ (dom
𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟0)) | 
| 191 | 183, 189,
190 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟0) ↾ (dom
𝑅 ∪ ran 𝑅)) = (𝑅↑𝑟0)) | 
| 192 | 180, 191 | eqtrid 2789 | . . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟0) ∘ ( I
↾ (dom 𝑅 ∪ ran
𝑅))) = (𝑅↑𝑟0)) | 
| 193 |  | simp1 1137 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑁 = 0) | 
| 194 | 193 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑁) = (𝑅↑𝑟0)) | 
| 195 |  | simp2 1138 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → 𝑀 = 0) | 
| 196 | 195 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑀) = (𝑅↑𝑟0)) | 
| 197 | 196, 184 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟𝑀) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 198 | 194, 197 | coeq12d 5875 | . . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = ((𝑅↑𝑟0) ∘ ( I
↾ (dom 𝑅 ∪ ran
𝑅)))) | 
| 199 | 193, 195 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = (0 + 0)) | 
| 200 |  | 00id 11436 | . . . . . . . . . . . . . 14
⊢ (0 + 0) =
0 | 
| 201 | 199, 200 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑁 + 𝑀) = 0) | 
| 202 | 201 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (𝑅↑𝑟(𝑁 + 𝑀)) = (𝑅↑𝑟0)) | 
| 203 | 192, 198,
202 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) | 
| 204 | 203 | a1d 25 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉) → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 205 | 204 | 3exp 1120 | . . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 206 | 205 | com12 32 | . . . . . . . 8
⊢ (𝑀 = 0 → (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 207 | 179, 206 | jaoi 858 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 208 | 2, 207 | sylbi 217 | . . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑁 = 0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 209 | 208 | com12 32 | . . . . 5
⊢ (𝑁 = 0 → (𝑀 ∈ ℕ0 → (𝑅 ∈ 𝑉 → (((𝑁 + 𝑀) = 1 → Rel 𝑅) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))))) | 
| 210 | 209 | 3impd 1349 | . . . 4
⊢ (𝑁 = 0 → ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅)) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 211 | 75, 210 | jaoi 858 | . . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅)) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 212 | 1, 211 | sylbi 217 | . 2
⊢ (𝑁 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅)) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀)))) | 
| 213 | 212 | imp 406 | 1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑅
∈ 𝑉 ∧ ((𝑁 + 𝑀) = 1 → Rel 𝑅))) → ((𝑅↑𝑟𝑁) ∘ (𝑅↑𝑟𝑀)) = (𝑅↑𝑟(𝑁 + 𝑀))) |