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 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
20 17 18 19 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
21 20 resiexd 
 |-  ( R e. V -> ( _I |` ( dom R u. ran R ) ) e. _V )
22 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 ) ) ) ) )
23 11 21 22 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 ) ) ) ) )
24 16 23 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 ) ) ) ) )
25 simp3r 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
26 0re 
 |-  0 e. RR
27 26 ltnri 
 |-  -. 0 < 0
28 9 15 breq12d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 0 < 0 ) )
29 27 28 mtbiri 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
30 29 iffalsed 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
31 25 30 15 3eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
32 31 oveq2d 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
33 32 13 eqtrd 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( _I |` ( dom R u. ran R ) ) )
34 8 24 33 3eqtr4a 
 |-  ( ( J = 0 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
35 34 3exp 
 |-  ( J = 0 -> ( K = 0 -> ( ( R e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
36 simp1 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 1 )
37 36 oveq2d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 1 ) )
38 simp3l 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> R e. V )
39 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
40 38 39 syl 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r 1 ) = R )
41 37 40 eqtrd 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = R )
42 simp2 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 0 )
43 41 42 oveq12d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r 0 ) )
44 simp3r 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
45 0lt1 
 |-  0 < 1
46 1re 
 |-  1 e. RR
47 26 46 ltnsymi 
 |-  ( 0 < 1 -> -. 1 < 0 )
48 45 47 mp1i 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. 1 < 0 )
49 36 42 breq12d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 1 < 0 ) )
50 48 49 mtbird 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
51 50 iffalsed 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
52 44 51 42 3eqtrd 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
53 52 oveq2d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
54 43 53 eqtr4d 
 |-  ( ( J = 1 /\ K = 0 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
55 54 3exp 
 |-  ( J = 1 -> ( K = 0 -> ( ( R e. 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 e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
57 ovex 
 |-  ( R ^r 0 ) e. _V
58 relexp1g 
 |-  ( ( R ^r 0 ) e. _V -> ( ( R ^r 0 ) ^r 1 ) = ( R ^r 0 ) )
59 57 58 mp1i 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r 0 ) ^r 1 ) = ( R ^r 0 ) )
60 simp1 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 0 )
61 60 oveq2d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 0 ) )
62 simp2 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 1 )
63 61 62 oveq12d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( ( R ^r 0 ) ^r 1 ) )
64 simp3r 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = if ( J < K , J , K ) )
65 60 62 breq12d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 0 < 1 ) )
66 45 65 mpbiri 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J < K )
67 66 iftrued 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = J )
68 64 67 60 3eqtrd 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 0 )
69 68 oveq2d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 0 ) )
70 59 63 69 3eqtr4d 
 |-  ( ( J = 0 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
71 70 3exp 
 |-  ( J = 0 -> ( K = 1 -> ( ( R e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) ) )
72 simp1 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> J = 1 )
73 72 oveq2d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = ( R ^r 1 ) )
74 simp3l 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> R e. V )
75 74 39 syl 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r 1 ) = R )
76 73 75 eqtrd 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r J ) = R )
77 simp2 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> K = 1 )
78 76 77 oveq12d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r 1 ) )
79 simp3r 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. 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 e. V /\ I = if ( J < K , J , K ) ) ) -> ( J < K <-> 1 < 1 ) )
82 80 81 mtbiri 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> -. J < K )
83 82 iffalsed 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> if ( J < K , J , K ) = K )
84 79 83 77 3eqtrd 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> I = 1 )
85 84 oveq2d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( R ^r I ) = ( R ^r 1 ) )
86 78 85 eqtr4d 
 |-  ( ( J = 1 /\ K = 1 /\ ( R e. V /\ I = if ( J < K , J , K ) ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
87 86 3exp 
 |-  ( J = 1 -> ( K = 1 -> ( ( R e. 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 e. 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 e. 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 e. V /\ I = if ( J < K , J , K ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) ) )
91 1 2 90 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 ) ) )
92 91 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 ) )