Metamath Proof Explorer

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 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )