relexpmulg - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > relexpmulg		Structured version Visualization version GIF version

Theorem relexpmulg 39424

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.)

**Assertion**
Ref	Expression
relexpmulg	⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))

**Proof of Theorem relexpmulg**
Step	Hyp	Ref	Expression
1		elnn0 11709	. . . 4 ⊢ (𝐽 ∈ ℕ₀ ↔ (𝐽 ∈ ℕ ∨ 𝐽 = 0))
2		elnn0 11709	. . . . . 6 ⊢ (𝐾 ∈ ℕ₀ ↔ (𝐾 ∈ ℕ ∨ 𝐾 = 0))
3		relexpmulnn 39423	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))
4	3	3adantl3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))
5	4	expcom 406	. . . . . . . 8 ⊢ ((𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))
6	5	expcom 406	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
7		simprr 760	. . . . . . . . . . . . 13 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = (𝐽 · 𝐾))
8		simpll 754	. . . . . . . . . . . . . 14 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐾 = 0)
9	8	oveq2d 6992	. . . . . . . . . . . . 13 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 𝐾) = (𝐽 · 0))
10		simplr 756	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℕ)
11	10	nncnd 11457	. . . . . . . . . . . . . 14 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐽 ∈ ℂ)
12	11	mul01d 10639	. . . . . . . . . . . . 13 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐽 · 0) = 0)
13	7, 9, 12	3eqtrd 2818	. . . . . . . . . . . 12 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → 𝐼 = 0)
14		simpl 475	. . . . . . . . . . . . 13 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → (𝐾 = 0 ∧ 𝐽 ∈ ℕ))
15		nnnle0 11473	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ ℕ → ¬ 𝐽 ≤ 0)
16	15	adantl 474	. . . . . . . . . . . . . 14 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 0)
17		simpl 475	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → 𝐾 = 0)
18	17	breq2d 4941	. . . . . . . . . . . . . 14 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝐽 ≤ 𝐾 ↔ 𝐽 ≤ 0))
19	16, 18	mtbird 317	. . . . . . . . . . . . 13 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ¬ 𝐽 ≤ 𝐾)
20	14, 19	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ 𝐽 ≤ 𝐾)
21	13, 20	jcn 329	. . . . . . . . . . 11 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ¬ (𝐼 = 0 → 𝐽 ≤ 𝐾))
22	21	pm2.21d 119	. . . . . . . . . 10 ⊢ (((𝐾 = 0 ∧ 𝐽 ∈ ℕ) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾))) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))
23	22	exp32 413	. . . . . . . . 9 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → (𝑅 ∈ 𝑉 → (𝐼 = (𝐽 · 𝐾) → ((𝐼 = 0 → 𝐽 ≤ 𝐾) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))))
24	23	3impd 1328	. . . . . . . 8 ⊢ ((𝐾 = 0 ∧ 𝐽 ∈ ℕ) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))
25	24	ex 405	. . . . . . 7 ⊢ (𝐾 = 0 → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
26	6, 25	jaoi 843	. . . . . 6 ⊢ ((𝐾 ∈ ℕ ∨ 𝐾 = 0) → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
27	2, 26	sylbi 209	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (𝐽 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
28		simplr 756	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐽 = 0)
29	28	oveq2d 6992	. . . . . . . . . 10 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑_𝑟𝐽) = (𝑅↑_𝑟0))
30		simpr1 1174	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝑅 ∈ 𝑉)
31		relexp0g 14242	. . . . . . . . . . 11 ⊢ (𝑅 ∈ 𝑉 → (𝑅↑_𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
32	30, 31	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑_𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
33	29, 32	eqtrd 2814	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑_𝑟𝐽) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
34	33	oveq1d 6991	. . . . . . . 8 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑_𝑟𝐾))
35		dmexg 7428	. . . . . . . . . . 11 ⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V)
36		rnexg 7429	. . . . . . . . . . 11 ⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V)
37		unexg 7289	. . . . . . . . . . 11 ⊢ ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
38	35, 36, 37	syl2anc 576	. . . . . . . . . 10 ⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
39	30, 38	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
40		simpll 754	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈ ℕ₀)
41		relexpiidm 39418	. . . . . . . . 9 ⊢ (((dom 𝑅 ∪ ran 𝑅) ∈ V ∧ 𝐾 ∈ ℕ₀) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑_𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
42	39, 40, 41	syl2anc 576	. . . . . . . 8 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (( I ↾ (dom 𝑅 ∪ ran 𝑅))↑_𝑟𝐾) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
43		simpr2 1175	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = (𝐽 · 𝐾))
44	28	oveq1d 6991	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝐽 · 𝐾) = (0 · 𝐾))
45	40	nn0cnd 11769	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐾 ∈ ℂ)
46	45	mul02d 10638	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (0 · 𝐾) = 0)
47	43, 44, 46	3eqtrd 2818	. . . . . . . . . 10 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → 𝐼 = 0)
48	47	oveq2d 6992	. . . . . . . . 9 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → (𝑅↑_𝑟𝐼) = (𝑅↑_𝑟0))
49	48, 32	eqtr2d 2815	. . . . . . . 8 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (𝑅↑_𝑟𝐼))
50	34, 42, 49	3eqtrd 2818	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) ∧ (𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾))) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))
51	50	ex 405	. . . . . 6 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))
52	51	ex 405	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (𝐽 = 0 → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
53	27, 52	jaod 845	. . . 4 ⊢ (𝐾 ∈ ℕ₀ → ((𝐽 ∈ ℕ ∨ 𝐽 = 0) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
54	1, 53	syl5bi 234	. . 3 ⊢ (𝐾 ∈ ℕ₀ → (𝐽 ∈ ℕ₀ → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))))
55	54	impcom 399	. 2 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀) → ((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼)))
56	55	impcom 399	1 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 = (𝐽 · 𝐾) ∧ (𝐼 = 0 → 𝐽 ≤ 𝐾)) ∧ (𝐽 ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀)) → ((𝑅↑_𝑟𝐽)↑_𝑟𝐾) = (𝑅↑_𝑟𝐼))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 ∨ wo 833 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 Vcvv 3415 ∪ cun 3827 class class class wbr 4929 I cid 5311 dom cdm 5407 ran crn 5408 ↾ cres 5409 (class class class)co 6976 0cc0 10335 · cmul 10340 ≤ cle 10475 ℕcn 11439 ℕ₀cn0 11707 ↑_𝑟crelexp 14240

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-om 7397 df-2nd 7502 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-nn 11440 df-n0 11708 df-z 11794 df-uz 12059 df-seq 13185 df-relexp 14241

This theorem is referenced by: (None)

W3C validator