Metamath Proof Explorer

Theorem relexp01min

Description: With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020)

Ref Expression
Assertion relexp01min ⊢R∈V∧I=ifJ<KJK∧J∈01∧K∈01→R↑rJ↑rK=R↑rI

Proof

Step Hyp Ref Expression
1 elpri ⊢J∈01→J=0∨J=1
2 elpri ⊢K∈01→K=0∨K=1
3 dmresi ⊢dom⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
4 rnresi ⊢ran⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
5 3 4 uneq12i ⊢dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R∪dom⁡R∪ran⁡R
6 unidm ⊢dom⁡R∪ran⁡R∪dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
7 5 6 eqtri ⊢dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
8 7 reseq2i ⊢I↾dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R=I↾dom⁡R∪ran⁡R
9 simp1 ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→J=0
10 9 oveq2d ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ=R↑r0
11 simp3l ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R∈V
12 relexp0g ⊢R∈V→R↑r0=I↾dom⁡R∪ran⁡R
13 11 12 syl ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑r0=I↾dom⁡R∪ran⁡R
14 10 13 eqtrd ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ=I↾dom⁡R∪ran⁡R
15 simp2 ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→K=0
16 14 15 oveq12d ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=I↾dom⁡R∪ran⁡R↑r0
17 dmexg ⊢R∈V→dom⁡R∈V
18 rnexg ⊢R∈V→ran⁡R∈V
19 17 18 unexd ⊢R∈V→dom⁡R∪ran⁡R∈V
20 19 resiexd ⊢R∈V→I↾dom⁡R∪ran⁡R∈V
21 relexp0g ⊢I↾dom⁡R∪ran⁡R∈V→I↾dom⁡R∪ran⁡R↑r0=I↾dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R
22 11 20 21 3syl ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→I↾dom⁡R∪ran⁡R↑r0=I↾dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R
23 16 22 eqtrd ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=I↾dom⁡I↾dom⁡R∪ran⁡R∪ran⁡I↾dom⁡R∪ran⁡R
24 simp3r ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→I=ifJ<KJK
25 0re ⊢0∈ℝ
26 25 ltnri ⊢¬0<0
27 9 15 breq12d ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→J<K↔0<0
28 26 27 mtbiri ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→¬J<K
29 28 iffalsed ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→ifJ<KJK=K
30 24 29 15 3eqtrd ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→I=0
31 30 oveq2d ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rI=R↑r0
32 31 13 eqtrd ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rI=I↾dom⁡R∪ran⁡R
33 8 23 32 3eqtr4a ⊢J=0∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
34 33 3exp ⊢J=0→K=0→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
35 simp1 ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→J=1
36 35 oveq2d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ=R↑r1
37 simp3l ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R∈V
38 37 relexp1d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑r1=R
39 36 38 eqtrd ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ=R
40 simp2 ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→K=0
41 39 40 oveq12d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑r0
42 simp3r ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→I=ifJ<KJK
43 0lt1 ⊢0<1
44 1re ⊢1∈ℝ
45 25 44 ltnsymi ⊢0<1→¬1<0
46 43 45 mp1i ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→¬1<0
47 35 40 breq12d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→J<K↔1<0
48 46 47 mtbird ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→¬J<K
49 48 iffalsed ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→ifJ<KJK=K
50 42 49 40 3eqtrd ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→I=0
51 50 oveq2d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑rI=R↑r0
52 41 51 eqtr4d ⊢J=1∧K=0∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
53 52 3exp ⊢J=1→K=0→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
54 34 53 jaoi ⊢J=0∨J=1→K=0→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
55 ovex ⊢R↑r0∈V
56 relexp1g ⊢R↑r0∈V→R↑r0↑r1=R↑r0
57 55 56 mp1i ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→R↑r0↑r1=R↑r0
58 simp1 ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→J=0
59 58 oveq2d ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ=R↑r0
60 simp2 ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→K=1
61 59 60 oveq12d ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑r0↑r1
62 simp3r ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→I=ifJ<KJK
63 58 60 breq12d ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→J<K↔0<1
64 43 63 mpbiri ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→J<K
65 64 iftrued ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→ifJ<KJK=J
66 62 65 58 3eqtrd ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→I=0
67 66 oveq2d ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→R↑rI=R↑r0
68 57 61 67 3eqtr4d ⊢J=0∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
69 68 3exp ⊢J=0→K=1→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
70 simp1 ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→J=1
71 70 oveq2d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ=R↑r1
72 simp3l ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R∈V
73 72 relexp1d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑r1=R
74 71 73 eqtrd ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ=R
75 simp2 ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→K=1
76 74 75 oveq12d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑r1
77 simp3r ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→I=ifJ<KJK
78 44 ltnri ⊢¬1<1
79 70 75 breq12d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→J<K↔1<1
80 78 79 mtbiri ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→¬J<K
81 80 iffalsed ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→ifJ<KJK=K
82 77 81 75 3eqtrd ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→I=1
83 82 oveq2d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑rI=R↑r1
84 76 83 eqtr4d ⊢J=1∧K=1∧R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
85 84 3exp ⊢J=1→K=1→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
86 69 85 jaoi ⊢J=0∨J=1→K=1→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
87 54 86 jaod ⊢J=0∨J=1→K=0∨K=1→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
88 87 imp ⊢J=0∨J=1∧K=0∨K=1→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
89 1 2 88 syl2an ⊢J∈01∧K∈01→R∈V∧I=ifJ<KJK→R↑rJ↑rK=R↑rI
90 89 impcom ⊢R∈V∧I=ifJ<KJK∧J∈01∧K∈01→R↑rJ↑rK=R↑rI