Metamath Proof Explorer

Theorem relexpxpmin

Description: The composition of powers of a Cartesian product of non-disjoint sets is the Cartesian product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpxpmin 
|- ( ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) /\ ( I = if ( J < K , J , K ) /\ J e. NN0 /\ K e. NN0 ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )
2 elnn0 
 |-  ( J e. NN0 <-> ( J e. NN \/ J = 0 ) )
3 ifeqor 
 |-  ( if ( J < K , J , K ) = J \/ if ( J < K , J , K ) = K )
4 andi 
 |-  ( ( I = if ( J < K , J , K ) /\ ( if ( J < K , J , K ) = J \/ if ( J < K , J , K ) = K ) ) <-> ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = J ) \/ ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = K ) ) )
5 4 biimpi 
 |-  ( ( I = if ( J < K , J , K ) /\ ( if ( J < K , J , K ) = J \/ if ( J < K , J , K ) = K ) ) -> ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = J ) \/ ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = K ) ) )
6 3 5 mpan2 
 |-  ( I = if ( J < K , J , K ) -> ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = J ) \/ ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = K ) ) )
7 eqtr 
 |-  ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = J ) -> I = J )
8 eqtr 
 |-  ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = K ) -> I = K )
9 7 8 orim12i 
 |-  ( ( ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = J ) \/ ( I = if ( J < K , J , K ) /\ if ( J < K , J , K ) = K ) ) -> ( I = J \/ I = K ) )
10 relexpxpnnidm 
 |-  ( K e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( A X. B ) ^r K ) = ( A X. B ) ) )
11 10 imp 
 |-  ( ( K e. NN /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r K ) = ( A X. B ) )
12 11 3ad2antl3 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r K ) = ( A X. B ) )
13 relexpxpnnidm 
 |-  ( J e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) ) )
14 13 imp 
 |-  ( ( J e. NN /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) )
15 14 3ad2antl2 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) )
16 15 oveq1d 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r K ) )
17 simpl1 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> I = J )
18 17 oveq2d 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( ( A X. B ) ^r J ) )
19 18 15 eqtrd 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( A X. B ) )
20 12 16 19 3eqtr4d 
 |-  ( ( ( I = J /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
21 20 3exp1 
 |-  ( I = J -> ( J e. NN -> ( K e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
22 14 3ad2antl2 
 |-  ( ( ( I = K /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) )
23 simpl1 
 |-  ( ( ( I = K /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> I = K )
24 23 eqcomd 
 |-  ( ( ( I = K /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> K = I )
25 22 24 oveq12d 
 |-  ( ( ( I = K /\ J e. NN /\ K e. NN ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
26 25 3exp1 
 |-  ( I = K -> ( J e. NN -> ( K e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
27 21 26 jaoi 
 |-  ( ( I = J \/ I = K ) -> ( J e. NN -> ( K e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
28 6 9 27 3syl 
 |-  ( I = if ( J < K , J , K ) -> ( J e. NN -> ( K e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
29 28 com13 
 |-  ( K e. NN -> ( J e. NN -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
30 simp3 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> I = if ( J < K , J , K ) )
31 simp2 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> J = 0 )
32 simp1 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> K e. NN )
33 32 nngt0d 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> 0 < K )
34 31 33 eqbrtrd 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> J < K )
35 34 iftrued 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> if ( J < K , J , K ) = J )
36 30 35 31 3eqtrd 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> I = 0 )
37 simpr1 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> A e. U )
38 simpr2 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> B e. V )
39 37 38 xpexd 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( A X. B ) e. _V )
40 dmexg 
 |-  ( ( A X. B ) e. _V -> dom ( A X. B ) e. _V )
41 rnexg 
 |-  ( ( A X. B ) e. _V -> ran ( A X. B ) e. _V )
42 40 41 jca 
 |-  ( ( A X. B ) e. _V -> ( dom ( A X. B ) e. _V /\ ran ( A X. B ) e. _V ) )
43 unexg 
 |-  ( ( dom ( A X. B ) e. _V /\ ran ( A X. B ) e. _V ) -> ( dom ( A X. B ) u. ran ( A X. B ) ) e. _V )
44 39 42 43 3syl 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( dom ( A X. B ) u. ran ( A X. B ) ) e. _V )
45 simpl1 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> K e. NN )
46 45 nnnn0d 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> K e. NN0 )
47 relexpiidm 
 |-  ( ( ( dom ( A X. B ) u. ran ( A X. B ) ) e. _V /\ K e. NN0 ) -> ( ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) ^r K ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
48 44 46 47 syl2anc 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) ^r K ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
49 simpl2 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> J = 0 )
50 49 oveq2d 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( ( A X. B ) ^r 0 ) )
51 relexp0g 
 |-  ( ( A X. B ) e. _V -> ( ( A X. B ) ^r 0 ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
52 39 51 syl 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r 0 ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
53 50 52 eqtrd 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
54 53 oveq1d 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) ^r K ) )
55 simpl3 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> I = 0 )
56 55 oveq2d 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( ( A X. B ) ^r 0 ) )
57 56 52 eqtrd 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( _I |` ( dom ( A X. B ) u. ran ( A X. B ) ) ) )
58 48 54 57 3eqtr4d 
 |-  ( ( ( K e. NN /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
59 58 ex 
 |-  ( ( K e. NN /\ J = 0 /\ I = 0 ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) )
60 36 59 syld3an3 
 |-  ( ( K e. NN /\ J = 0 /\ I = if ( J < K , J , K ) ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) )
61 60 3exp 
 |-  ( K e. NN -> ( J = 0 -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
62 29 61 jaod 
 |-  ( K e. NN -> ( ( J e. NN \/ J = 0 ) -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
63 2 62 syl5bi 
 |-  ( K e. NN -> ( J e. NN0 -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
64 simp1 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> K = 0 )
65 2 biimpi 
 |-  ( J e. NN0 -> ( J e. NN \/ J = 0 ) )
66 65 3ad2ant2 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> ( J e. NN \/ J = 0 ) )
67 simp3 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> I = if ( J < K , J , K ) )
68 nn0nlt0 
 |-  ( J e. NN0 -> -. J < 0 )
69 68 3ad2ant2 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> -. J < 0 )
70 64 breq2d 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> ( J < K <-> J < 0 ) )
71 69 70 mtbird 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> -. J < K )
72 71 iffalsed 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> if ( J < K , J , K ) = K )
73 67 72 64 3eqtrd 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> I = 0 )
74 13 3ad2ant2 
 |-  ( ( K = 0 /\ J e. NN /\ I = 0 ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) ) )
75 74 imp 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( A X. B ) )
76 75 oveq1d 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r 0 ) = ( ( A X. B ) ^r 0 ) )
77 simpl1 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> K = 0 )
78 77 oveq2d 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( ( A X. B ) ^r J ) ^r 0 ) )
79 simpl3 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> I = 0 )
80 79 oveq2d 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( ( A X. B ) ^r 0 ) )
81 76 78 80 3eqtr4d 
 |-  ( ( ( K = 0 /\ J e. NN /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
82 81 3exp1 
 |-  ( K = 0 -> ( J e. NN -> ( I = 0 -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
83 simpr1 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> A e. U )
84 simpr2 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> B e. V )
85 83 84 xpexd 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( A X. B ) e. _V )
86 relexp0idm 
 |-  ( ( A X. B ) e. _V -> ( ( ( A X. B ) ^r 0 ) ^r 0 ) = ( ( A X. B ) ^r 0 ) )
87 85 86 syl 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r 0 ) ^r 0 ) = ( ( A X. B ) ^r 0 ) )
88 simpl2 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> J = 0 )
89 88 oveq2d 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r J ) = ( ( A X. B ) ^r 0 ) )
90 simpl1 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> K = 0 )
91 89 90 oveq12d 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( ( A X. B ) ^r 0 ) ^r 0 ) )
92 simpl3 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> I = 0 )
93 92 oveq2d 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( A X. B ) ^r I ) = ( ( A X. B ) ^r 0 ) )
94 87 91 93 3eqtr4d 
 |-  ( ( ( K = 0 /\ J = 0 /\ I = 0 ) /\ ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
95 94 3exp1 
 |-  ( K = 0 -> ( J = 0 -> ( I = 0 -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
96 82 95 jaod 
 |-  ( K = 0 -> ( ( J e. NN \/ J = 0 ) -> ( I = 0 -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
97 64 66 73 96 syl3c 
 |-  ( ( K = 0 /\ J e. NN0 /\ I = if ( J < K , J , K ) ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) )
98 97 3exp 
 |-  ( K = 0 -> ( J e. NN0 -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
99 63 98 jaoi 
 |-  ( ( K e. NN \/ K = 0 ) -> ( J e. NN0 -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
100 1 99 sylbi 
 |-  ( K e. NN0 -> ( J e. NN0 -> ( I = if ( J < K , J , K ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) ) ) )
101 100 3imp31 
 |-  ( ( I = if ( J < K , J , K ) /\ J e. NN0 /\ K e. NN0 ) -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) ) )
102 101 impcom 
 |-  ( ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) /\ ( I = if ( J < K , J , K ) /\ J e. NN0 /\ K e. NN0 ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )