Metamath Proof Explorer

Theorem relexpaddss

Description: The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where R is a relation as shown by relexpaddd or when the sum of the powers isn't 1 as shown by relexpaddg . (Contributed by RP, 3-Jun-2020)

Ref Expression
Assertion relexpaddss ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
2 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
3 2 biimpi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
4 relexpaddnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
5 eqimss ⊢ ( ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
6 4 5 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
7 6 3exp ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
8 elnn1uz2 ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
9 relco ⊢ Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 )
10 dfrel2 ⊢ ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ↔ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
11 10 biimpi ⊢ ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) → ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
12 9 11 ax-mp ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 )
13 cnvco ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
14 cnvresid ⊢ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
15 14 coeq2i ⊢ ( ◡ 𝑅 ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
16 coires1 ⊢ ( ◡ 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
17 13 15 16 3eqtri ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
18 eqimss ⊢ ( ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
19 17 18 ax-mp ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
20 cnvss ⊢ ( ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
21 19 20 ax-mp ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
22 resss ⊢ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ 𝑅
23 cnvss ⊢ ( ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ 𝑅 → ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ ◡ 𝑅 )
24 22 23 ax-mp ⊢ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ ◡ 𝑅
25 21 24 sstri ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ◡ 𝑅
26 12 25 eqsstrri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ◡ 𝑅
27 cnvcnvss ⊢ ◡ ◡ 𝑅 ⊆ 𝑅
28 26 27 sstri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ 𝑅
29 28 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ 𝑅 )
30 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
31 30 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
32 relexp0g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
33 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34 31 33 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
35 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 1 )
36 35 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 1 ) )
37 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
38 37 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
39 36 38 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = 𝑅 )
40 34 39 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
41 30 35 oveq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 1 ) )
42 1cnd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 1 ∈ ℂ )
43 42 addlidd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 1 ) = 1 )
44 41 43 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 1 )
45 44 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 1 ) )
46 45 38 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = 𝑅 )
47 29 40 46 3sstr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
48 47 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 = 1 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
49 coires1 ⊢ ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
50 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
51 cnvexg ⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
52 51 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ 𝑅 ∈ V )
53 relexpuzrel ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ◡ 𝑅 ∈ V ) → Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) )
54 50 52 53 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) )
55 eluz2nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
56 50 55 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℕ )
57 relexpnndm ⊢ ( ( 𝑀 ∈ ℕ ∧ ◡ 𝑅 ∈ V ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ dom ◡ 𝑅 )
58 56 52 57 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ dom ◡ 𝑅 )
59 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
60 ssun2 ⊢ ran 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
61 59 60 eqsstrri ⊢ dom ◡ 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
62 58 61 sstrdi ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
63 relssres ⊢ ( ( Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) ∧ dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
64 54 62 63 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
65 49 64 eqtrid ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
66 cnvco ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ◡ ( 𝑅 ↑𝑟 𝑀 ) ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
67 simp3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
68 eluzge2nn0 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ0 )
69 50 68 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℕ0 )
70 67 69 relexpcnvd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑀 ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
71 14 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
72 70 71 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ◡ ( 𝑅 ↑𝑟 𝑀 ) ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
73 66 72 eqtrid ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
74 65 73 70 3eqtr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) )
75 relco ⊢ Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) )
76 relexpuzrel ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑀 ) )
77 76 3adant1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑀 ) )
78 cnveqb ⊢ ( ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ∧ Rel ( 𝑅 ↑𝑟 𝑀 ) ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) ↔ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) ) )
79 75 77 78 sylancr ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) ↔ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) ) )
80 74 79 mpbird ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) )
81 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
82 81 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
83 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
84 82 83 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
85 84 coeq1d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) )
86 81 oveq1d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 𝑀 ) )
87 eluzelcn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℂ )
88 50 87 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℂ )
89 88 addlidd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 𝑀 ) = 𝑀 )
90 86 89 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 𝑀 )
91 90 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) )
92 80 85 91 3eqtr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
93 92 5 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
94 93 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
95 48 94 jaod ⊢ ( 𝑁 = 0 → ( ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
96 8 95 biimtrid ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
97 7 96 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
98 3 97 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
99 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
100 99 biimpi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
101 coires1 ⊢ ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
102 resss ⊢ ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑅
103 101 102 eqsstri ⊢ ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ⊆ 𝑅
104 103 a1i ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ⊆ 𝑅 )
105 simp1 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 1 )
106 105 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 1 ) )
107 37 3ad2ant3 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
108 106 107 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = 𝑅 )
109 simp2 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
110 109 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
111 32 3ad2ant3 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
112 110 111 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
113 108 112 coeq12d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
114 105 109 oveq12d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 1 + 0 ) )
115 1cnd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 1 ∈ ℂ )
116 115 addridd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 1 + 0 ) = 1 )
117 114 116 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 1 )
118 117 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 1 ) )
119 118 107 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = 𝑅 )
120 104 113 119 3sstr4d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
121 120 3exp ⊢ ( 𝑁 = 1 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
122 coires1 ⊢ ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
123 relexpuzrel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
124 123 3adant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
125 simp1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
126 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
127 125 126 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℕ )
128 simp3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
129 relexpnndm ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )
130 127 128 129 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )
131 ssun1 ⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
132 130 131 sstrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
133 relssres ⊢ ( ( Rel ( 𝑅 ↑𝑟 𝑁 ) ∧ dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
134 124 132 133 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
135 122 134 eqtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
136 simp2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
137 136 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
138 32 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
139 137 138 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
140 139 coeq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
141 136 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 𝑁 + 0 ) )
142 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
143 125 142 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℂ )
144 143 addridd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 0 ) = 𝑁 )
145 141 144 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 𝑁 )
146 145 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
147 135 140 146 3eqtr4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
148 147 5 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
149 148 3exp ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
150 121 149 jaoi ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
151 100 150 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
152 coires1 ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
153 resres ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) )
154 inidm ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
155 154 reseq2i ⊢ ( I ↾ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
156 152 153 155 3eqtri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
157 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
158 157 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
159 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
160 158 159 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
161 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
162 161 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
163 162 159 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
164 160 163 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
165 157 161 oveq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 0 ) )
166 00id ⊢ ( 0 + 0 ) = 0
167 166 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 0 ) = 0 )
168 165 167 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 0 )
169 168 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 0 ) )
170 169 159 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
171 156 164 170 3eqtr4a ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
172 171 5 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
173 172 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
174 151 173 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
175 3 174 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
176 98 175 jaod ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
177 1 176 biimtrid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
178 177 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )