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