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 U B V A B I = if J < K J K J 0 K 0 A × B r J r K = A × B r I

Proof

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