Metamath Proof Explorer

Theorem relexpaddg

Description: Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020)

Ref Expression
Assertion relexpaddg ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )

Proof

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