relexpmulg

Description: With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020)

		Ref	Expression
	Assertion	relexpmulg	$⊢ ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \land (J \in ℕ_{0} \land K \in ℕ_{0})) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ J \in ℕ_{0} \leftrightarrow (J \in ℕ \lor J = 0)$
2		elnn0	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℕ \lor K = 0)$
3		relexpmulnn	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$
4	3	3adantl3	$⊢ ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \land (J \in ℕ \land K \in ℕ)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$
5	4	expcom	$⊢ (J \in ℕ \land K \in ℕ) \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)$
6	5	expcom	$⊢ K \in ℕ \to (J \in ℕ \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
7		simprr	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to I = J K$
8		simpll	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to K = 0$
9	8	oveq2d	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to J K = J \cdot 0$
10		simplr	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to J \in ℕ$
11	10	nncnd	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to J \in ℂ$
12	11	mul01d	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to J \cdot 0 = 0$
13	7 9 12	3eqtrd	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to I = 0$
14		simpl	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to (K = 0 \land J \in ℕ)$
15		nnnle0	$⊢ J \in ℕ \to \neg J \leq 0$
16	15	adantl	$⊢ (K = 0 \land J \in ℕ) \to \neg J \leq 0$
17		simpl	$⊢ (K = 0 \land J \in ℕ) \to K = 0$
18	17	breq2d	$⊢ (K = 0 \land J \in ℕ) \to (J \leq K \leftrightarrow J \leq 0)$
19	16 18	mtbird	$⊢ (K = 0 \land J \in ℕ) \to \neg J \leq K$
20	14 19	syl	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to \neg J \leq K$
21	13 20	jcnd	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to \neg (I = 0 \to J \leq K)$
22	21	pm2.21d	$⊢ ((K = 0 \land J \in ℕ) \land (R \in V \land I = J K)) \to ((I = 0 \to J \leq K) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)$
23	22	exp32	$⊢ (K = 0 \land J \in ℕ) \to (R \in V \to (I = J K \to ((I = 0 \to J \leq K) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)))$
24	23	3impd	$⊢ (K = 0 \land J \in ℕ) \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)$
25	24	ex	$⊢ K = 0 \to (J \in ℕ \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
26	6 25	jaoi	$⊢ (K \in ℕ \lor K = 0) \to (J \in ℕ \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
27	2 26	sylbi	$⊢ K \in ℕ_{0} \to (J \in ℕ \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
28		simplr	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to J = 0$
29	28	oveq2d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to R ↑_{r} J = R ↑_{r} 0$
30		simpr1	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to R \in V$
31		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
32	30 31	syl	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
33	29 32	eqtrd	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to R ↑_{r} J = {I ↾}_{(dom R \cup ran R)}$
34	33	oveq1d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to (R ↑_{r} J) ↑_{r} K = ({I ↾}_{(dom R \cup ran R)}) ↑_{r} K$
35		dmexg	$⊢ R \in V \to dom R \in V$
36		rnexg	$⊢ R \in V \to ran R \in V$
37		unexg	$⊢ (dom R \in V \land ran R \in V) \to dom R \cup ran R \in V$
38	35 36 37	syl2anc	$⊢ R \in V \to dom R \cup ran R \in V$
39	30 38	syl	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to dom R \cup ran R \in V$
40		simpll	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to K \in ℕ_{0}$
41		relexpiidm	$⊢ (dom R \cup ran R \in V \land K \in ℕ_{0}) \to ({I ↾}_{(dom R \cup ran R)}) ↑_{r} K = {I ↾}_{(dom R \cup ran R)}$
42	39 40 41	syl2anc	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to ({I ↾}_{(dom R \cup ran R)}) ↑_{r} K = {I ↾}_{(dom R \cup ran R)}$
43		simpr2	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to I = J K$
44	28	oveq1d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to J K = 0 \cdot K$
45	40	nn0cnd	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to K \in ℂ$
46	45	mul02d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to 0 \cdot K = 0$
47	43 44 46	3eqtrd	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to I = 0$
48	47	oveq2d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to R ↑_{r} I = R ↑_{r} 0$
49	48 32	eqtr2d	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to {I ↾}_{(dom R \cup ran R)} = R ↑_{r} I$
50	34 42 49	3eqtrd	$⊢ ((K \in ℕ_{0} \land J = 0) \land (R \in V \land I = J K \land (I = 0 \to J \leq K))) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$
51	50	ex	$⊢ (K \in ℕ_{0} \land J = 0) \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)$
52	51	ex	$⊢ K \in ℕ_{0} \to (J = 0 \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
53	27 52	jaod	$⊢ K \in ℕ_{0} \to ((J \in ℕ \lor J = 0) \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
54	1 53	syl5bi	$⊢ K \in ℕ_{0} \to (J \in ℕ_{0} \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I))$
55	54	impcom	$⊢ (J \in ℕ_{0} \land K \in ℕ_{0}) \to ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I)$
56	55	impcom	$⊢ ((R \in V \land I = J K \land (I = 0 \to J \leq K)) \land (J \in ℕ_{0} \land K \in ℕ_{0})) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$

Metamath Proof Explorer

Theorem relexpmulg

Proof