Theorem 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	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝐽 ∈ ℕ0 ↔ ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) )
2		elnn0	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
3		relexpmulnn	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
4	3	3adantl3	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
5	4	expcom	⊢ ( ( 𝐽 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
6	5	expcom	⊢ ( 𝐾 ∈ ℕ → ( 𝐽 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
7		simprr	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → 𝐼 = ( 𝐽 · 𝐾 ) )
8		simpll	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → 𝐾 = 0 )
9	8	oveq2d	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ( 𝐽 · 𝐾 ) = ( 𝐽 · 0 ) )
10		simplr	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → 𝐽 ∈ ℕ )
11	10	nncnd	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → 𝐽 ∈ ℂ )
12	11	mul01d	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ( 𝐽 · 0 ) = 0 )
13	7 9 12	3eqtrd	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → 𝐼 = 0 )
14		simpl	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) )
15		nnnle0	⊢ ( 𝐽 ∈ ℕ → ¬ 𝐽 ≤ 0 )
16	15	adantl	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → ¬ 𝐽 ≤ 0 )
17		simpl	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → 𝐾 = 0 )
18	17	breq2d	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → ( 𝐽 ≤ 𝐾 ↔ 𝐽 ≤ 0 ) )
19	16 18	mtbird	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → ¬ 𝐽 ≤ 𝐾 )
20	14 19	syl	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ¬ 𝐽 ≤ 𝐾 )
21	13 20	jcnd	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ¬ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) )
22	21	pm2.21d	⊢ ( ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ) ) → ( ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
23	22	exp32	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → ( 𝑅 ∈ 𝑉 → ( 𝐼 = ( 𝐽 · 𝐾 ) → ( ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) ) )
24	23	3impd	⊢ ( ( 𝐾 = 0 ∧ 𝐽 ∈ ℕ ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
25	24	ex	⊢ ( 𝐾 = 0 → ( 𝐽 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
26	6 25	jaoi	⊢ ( ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) → ( 𝐽 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
27	2 26	sylbi	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
28		simplr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐽 = 0 )
29	28	oveq2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( 𝑅 ↑𝑟 0 ) )
30		simpr1	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝑅 ∈ 𝑉 )
31		relexp0g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
32	30 31	syl	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
33	29 32	eqtrd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐽 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34	33	oveq1d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 𝐾 ) )
35		dmexg	⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
36		rnexg	⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
37	35 36	unexd	⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
38	30 37	syl	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
39		simpll	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐾 ∈ ℕ0 )
40		relexpiidm	⊢ ( ( ( dom 𝑅 ∪ ran 𝑅 ) ∈ V ∧ 𝐾 ∈ ℕ0 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
41	38 39 40	syl2anc	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
42		simpr2	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐼 = ( 𝐽 · 𝐾 ) )
43	28	oveq1d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝐽 · 𝐾 ) = ( 0 · 𝐾 ) )
44	39	nn0cnd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐾 ∈ ℂ )
45	44	mul02d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 0 · 𝐾 ) = 0 )
46	42 43 45	3eqtrd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐼 = 0 )
47	46	oveq2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 0 ) )
48	47 32	eqtr2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝐼 ) )
49	34 41 48	3eqtrd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
50	49	ex	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
51	50	ex	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
52	27 51	jaod	⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
53	1 52	biimtrid	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 ∈ ℕ0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
54	53	impcom	⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
55	54	impcom	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )