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 unexg ⊢ ( ( dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
38 35 36 37 syl2anc ⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
39 30 38 syl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
40 simpll ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐾 ∈ ℕ0 )
41 relexpiidm ⊢ ( ( ( dom 𝑅 ∪ ran 𝑅 ) ∈ V ∧ 𝐾 ∈ ℕ0 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
42 39 40 41 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↑𝑟 𝐾 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
43 simpr2 ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐼 = ( 𝐽 · 𝐾 ) )
44 28 oveq1d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝐽 · 𝐾 ) = ( 0 · 𝐾 ) )
45 40 nn0cnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐾 ∈ ℂ )
46 45 mul02d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 0 · 𝐾 ) = 0 )
47 43 44 46 3eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → 𝐼 = 0 )
48 47 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( 𝑅 ↑𝑟 𝐼 ) = ( 𝑅 ↑𝑟 0 ) )
49 48 32 eqtr2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝐼 ) )
50 34 42 49 3eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )
51 50 ex ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐽 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
52 51 ex ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
53 27 52 jaod ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐽 ∈ ℕ ∨ 𝐽 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
54 1 53 syl5bi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐽 ∈ ℕ0 → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) ) )
55 54 impcom ⊢ ( ( 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) ) )
56 55 impcom ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 = ( 𝐽 · 𝐾 ) ∧ ( 𝐼 = 0 → 𝐽 ≤ 𝐾 ) ) ∧ ( 𝐽 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( 𝑅 ↑𝑟 𝐽 ) ↑𝑟 𝐾 ) = ( 𝑅 ↑𝑟 𝐼 ) )