relexpmulnn

Description: With exponents limited to the counting numbers, 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	relexpmulnn	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 1 \to (R ↑_{r} J) ↑_{r} x = (R ↑_{r} J) ↑_{r} 1$
2		oveq2	$⊢ x = 1 \to J x = J \cdot 1$
3	2	oveq2d	$⊢ x = 1 \to R ↑_{r} J x = R ↑_{r} J \cdot 1$
4	1 3	eqeq12d	$⊢ x = 1 \to ((R ↑_{r} J) ↑_{r} x = R ↑_{r} J x \leftrightarrow (R ↑_{r} J) ↑_{r} 1 = R ↑_{r} J \cdot 1)$
5	4	imbi2d	$⊢ x = 1 \to (((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} x = R ↑_{r} J x) \leftrightarrow ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} 1 = R ↑_{r} J \cdot 1))$
6		oveq2	$⊢ x = y \to (R ↑_{r} J) ↑_{r} x = (R ↑_{r} J) ↑_{r} y$
7		oveq2	$⊢ x = y \to J x = J y$
8	7	oveq2d	$⊢ x = y \to R ↑_{r} J x = R ↑_{r} J y$
9	6 8	eqeq12d	$⊢ x = y \to ((R ↑_{r} J) ↑_{r} x = R ↑_{r} J x \leftrightarrow (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y)$
10	9	imbi2d	$⊢ x = y \to (((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} x = R ↑_{r} J x) \leftrightarrow ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y))$
11		oveq2	$⊢ x = y + 1 \to (R ↑_{r} J) ↑_{r} x = (R ↑_{r} J) ↑_{r} (y + 1)$
12		oveq2	$⊢ x = y + 1 \to J x = J (y + 1)$
13	12	oveq2d	$⊢ x = y + 1 \to R ↑_{r} J x = R ↑_{r} J (y + 1)$
14	11 13	eqeq12d	$⊢ x = y + 1 \to ((R ↑_{r} J) ↑_{r} x = R ↑_{r} J x \leftrightarrow (R ↑_{r} J) ↑_{r} (y + 1) = R ↑_{r} J (y + 1))$
15	14	imbi2d	$⊢ x = y + 1 \to (((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} x = R ↑_{r} J x) \leftrightarrow ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} (y + 1) = R ↑_{r} J (y + 1)))$
16		oveq2	$⊢ x = K \to (R ↑_{r} J) ↑_{r} x = (R ↑_{r} J) ↑_{r} K$
17		oveq2	$⊢ x = K \to J x = J K$
18	17	oveq2d	$⊢ x = K \to R ↑_{r} J x = R ↑_{r} J K$
19	16 18	eqeq12d	$⊢ x = K \to ((R ↑_{r} J) ↑_{r} x = R ↑_{r} J x \leftrightarrow (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K)$
20	19	imbi2d	$⊢ x = K \to (((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} x = R ↑_{r} J x) \leftrightarrow ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K))$
21		ovexd	$⊢ (J \in ℕ \land R \in V \land I = J K) \to R ↑_{r} J \in V$
22	21	relexp1d	$⊢ (J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} 1 = R ↑_{r} J$
23		simp1	$⊢ (J \in ℕ \land R \in V \land I = J K) \to J \in ℕ$
24		nnre	$⊢ J \in ℕ \to J \in ℝ$
25		ax-1rid	$⊢ J \in ℝ \to J \cdot 1 = J$
26	23 24 25	3syl	$⊢ (J \in ℕ \land R \in V \land I = J K) \to J \cdot 1 = J$
27	26	eqcomd	$⊢ (J \in ℕ \land R \in V \land I = J K) \to J = J \cdot 1$
28	27	oveq2d	$⊢ (J \in ℕ \land R \in V \land I = J K) \to R ↑_{r} J = R ↑_{r} J \cdot 1$
29	22 28	eqtrd	$⊢ (J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} 1 = R ↑_{r} J \cdot 1$
30		ovex	$⊢ R ↑_{r} J \in V$
31		simp1	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to y \in ℕ$
32		relexpsucnnr	$⊢ (R ↑_{r} J \in V \land y \in ℕ) \to (R ↑_{r} J) ↑_{r} (y + 1) = ((R ↑_{r} J) ↑_{r} y) \circ (R ↑_{r} J)$
33	30 31 32	sylancr	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to (R ↑_{r} J) ↑_{r} (y + 1) = ((R ↑_{r} J) ↑_{r} y) \circ (R ↑_{r} J)$
34		simp3	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y$
35	34	coeq1d	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to ((R ↑_{r} J) ↑_{r} y) \circ (R ↑_{r} J) = (R ↑_{r} J y) \circ (R ↑_{r} J)$
36		simp21	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J \in ℕ$
37	36 31	nnmulcld	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J y \in ℕ$
38		simp22	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to R \in V$
39		relexpaddnn	$⊢ (J y \in ℕ \land J \in ℕ \land R \in V) \to (R ↑_{r} J y) \circ (R ↑_{r} J) = R ↑_{r} (J y + J)$
40	37 36 38 39	syl3anc	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to (R ↑_{r} J y) \circ (R ↑_{r} J) = R ↑_{r} (J y + J)$
41	35 40	eqtrd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to ((R ↑_{r} J) ↑_{r} y) \circ (R ↑_{r} J) = R ↑_{r} (J y + J)$
42	36	nncnd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J \in ℂ$
43	31	nncnd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to y \in ℂ$
44		1cnd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to 1 \in ℂ$
45	42 43 44	adddid	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J (y + 1) = J y + J \cdot 1$
46	42	mulid1d	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J \cdot 1 = J$
47	46	oveq2d	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J y + J \cdot 1 = J y + J$
48	45 47	eqtr2d	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to J y + J = J (y + 1)$
49	48	oveq2d	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to R ↑_{r} (J y + J) = R ↑_{r} J (y + 1)$
50	41 49	eqtrd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to ((R ↑_{r} J) ↑_{r} y) \circ (R ↑_{r} J) = R ↑_{r} J (y + 1)$
51	33 50	eqtrd	$⊢ (y \in ℕ \land (J \in ℕ \land R \in V \land I = J K) \land (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to (R ↑_{r} J) ↑_{r} (y + 1) = R ↑_{r} J (y + 1)$
52	51	3exp	$⊢ y \in ℕ \to ((J \in ℕ \land R \in V \land I = J K) \to ((R ↑_{r} J) ↑_{r} y = R ↑_{r} J y \to (R ↑_{r} J) ↑_{r} (y + 1) = R ↑_{r} J (y + 1)))$
53	52	a2d	$⊢ y \in ℕ \to (((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} y = R ↑_{r} J y) \to ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} (y + 1) = R ↑_{r} J (y + 1)))$
54	5 10 15 20 29 53	nnind	$⊢ K \in ℕ \to ((J \in ℕ \land R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K)$
55	54	3expd	$⊢ K \in ℕ \to (J \in ℕ \to (R \in V \to (I = J K \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K)))$
56	55	impcom	$⊢ (J \in ℕ \land K \in ℕ) \to (R \in V \to (I = J K \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K))$
57	56	impd	$⊢ (J \in ℕ \land K \in ℕ) \to ((R \in V \land I = J K) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K)$
58	57	impcom	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} J K$
59		simplr	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to I = J K$
60	59	eqcomd	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to J K = I$
61	60	oveq2d	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to R ↑_{r} J K = R ↑_{r} I$
62	58 61	eqtrd	$⊢ ((R \in V \land I = J K) \land (J \in ℕ \land K \in ℕ)) \to (R ↑_{r} J) ↑_{r} K = R ↑_{r} I$

Metamath Proof Explorer

Theorem relexpmulnn

Proof