# Metamath Proof Explorer

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 ${⊢}\left({N}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\wedge {R}\in {V}\right)\to \left({R}{↑}_{r}{N}\right)\circ \left({R}{↑}_{r}{M}\right)\subseteq {R}{↑}_{r}\left({N}+{M}\right)$

### Proof

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