relexpxpmin

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

		Ref	Expression
	Assertion	relexpxpmin	$⊢ ((A \in U \land B \in V \land A \cap B \neq \emptyset) \land (I = if (J < K, J, K) \land J \in ℕ_{0} \land K \in ℕ_{0})) \to ((A \times B) ↑_{r} J) ↑_{r} K = (A \times B) ↑_{r} I$

Proof

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

Metamath Proof Explorer

Theorem relexpxpmin

Proof