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 e. V /\ I = if ( J < K , J , K ) ) /\ ( J e. { 0 , 1 } /\ K e. { 0 , 1 } ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( J e. { 0 , 1 } -> ( J = 0 \/ J = 1 ) )
2 elpri 
 |-  ( K e. { 0 , 1 } -> ( K = 0 \/ K = 1 ) )
3 dmresi 
 |-  dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
4 rnresi 
 |-  ran ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
5 3 4 uneq12i 
 |-  ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) = ( ( dom R u. ran R ) u. ( dom R u. ran R ) )
6 unidm 
 |-  ( ( dom R u. ran R ) u. ( dom R u. ran R ) ) = ( dom R u. ran R )
7 5 6 eqtri 
 |-  ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) = ( dom R u. ran R )
8 7 reseq2i 
 |-  ( _I |` ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) ) = ( _I |` ( dom R u. ran R ) )
9 simp1 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 0 )
10 9 oveq2d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 0 ) )
11 simp3l 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> R e. V )
12 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
13 11 12 syl 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
14 10 13 eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( _I |` ( dom R u. ran R ) ) )
15 simp2 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 0 )
16 14 15 oveq12d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( ( _I |` ( dom R u. ran R ) ) ^r 0 ) )
17 dmexg 
 |-  ( R e. V -> dom R e. _V )
18 rnexg 
 |-  ( R e. V -> ran R e. _V )
19 17 18 unexd 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
20 19 resiexd 
 |-  ( R e. V -> ( _I |` ( dom R u. ran R ) ) e. _V )
21 relexp0g 
 |-  ( ( _I |` ( dom R u. ran R ) ) e. _V -> ( ( _I |` ( dom R u. ran R ) ) ^r 0 ) = ( _I |` ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) ) )
22 11 20 21 3syl 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( _I |` ( dom R u. ran R ) ) ^r 0 ) = ( _I |` ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) ) )
23 16 22 eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( _I |` ( dom ( _I |` ( dom R u. ran R ) ) u. ran ( _I |` ( dom R u. ran R ) ) ) ) )
24 simp3r 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
25 0re 
 |-  0 e. RR
26 25 ltnri 
 |-  -. 0 < 0
27 9 15 breq12d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 0 < 0 ) )
28 26 27 mtbiri 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
29 28 iffalsed 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
30 24 29 15 3eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
31 30 oveq2d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
32 31 13 eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( _I |` ( dom R u. ran R ) ) )
33 8 23 32 3eqtr4a 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
34 33 3exp 
 |-  ( J = 0 -> ( K = 0 -> ( ( R e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
35 simp1 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 1 )
36 35 oveq2d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 1 ) )
37 simp3l 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> R e. V )
38 37 relexp1d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r 1 ) = R )
39 36 38 eqtrd 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = R )
40 simp2 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 0 )
41 39 40 oveq12d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r 0 ) )
42 simp3r 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
43 0lt1 
 |-  0 < 1
44 1re 
 |-  1 e. RR
45 25 44 ltnsymi 
 |-  ( 0 < 1 -> -. 1 < 0 )
46 43 45 mp1i 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. 1 < 0 )
47 35 40 breq12d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 1 < 0 ) )
48 46 47 mtbird 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
49 48 iffalsed 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
50 42 49 40 3eqtrd 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
51 50 oveq2d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
52 41 51 eqtr4d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
53 52 3exp 
 |-  ( J = 1 -> ( K = 0 -> ( ( R e. 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 e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
55 ovex 
 |-  ( R ^r 0 ) e. _V
56 relexp1g 
 |-  ( ( R ^r 0 ) e. _V -> ( ( R ^r 0 ) ^r 1 ) = ( R ^r 0 ) )
57 55 56 mp1i 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r 0 ) ^r 1 ) = ( R ^r 0 ) )
58 simp1 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 0 )
59 58 oveq2d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 0 ) )
60 simp2 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 1 )
61 59 60 oveq12d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( ( R ^r 0 ) ^r 1 ) )
62 simp3r 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
63 58 60 breq12d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 0 < 1 ) )
64 43 63 mpbiri 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J < K )
65 64 iftrued 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = J )
66 62 65 58 3eqtrd 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
67 66 oveq2d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
68 57 61 67 3eqtr4d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
69 68 3exp 
 |-  ( J = 0 -> ( K = 1 -> ( ( R e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
70 simp1 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 1 )
71 70 oveq2d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 1 ) )
72 simp3l 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> R e. V )
73 72 relexp1d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r 1 ) = R )
74 71 73 eqtrd 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = R )
75 simp2 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 1 )
76 74 75 oveq12d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r 1 ) )
77 simp3r 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. 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 e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 1 < 1 ) )
80 78 79 mtbiri 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
81 80 iffalsed 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
82 77 81 75 3eqtrd 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 1 )
83 82 oveq2d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 1 ) )
84 76 83 eqtr4d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
85 84 3exp 
 |-  ( J = 1 -> ( K = 1 -> ( ( R e. 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 e. 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 e. 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 e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
89 1 2 88 syl2an 
 |-  ( ( J e. { 0 , 1 } /\ K e. { 0 , 1 } ) -> ( ( R e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
90 89 impcom 
 |-  ( ( ( R e. V /\ I = if ( J < K , J , K ) ) /\ ( J e. { 0 , 1 } /\ K e. { 0 , 1 } ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )