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 = if J < K J K ∧ J ∈ 0 1 ∧ K ∈ 0 1 → R ↑ r J ↑ r K = R ↑ r I

Proof

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