Theorem relexpnul

Description: If the domain and range of powers of a relation are disjoint then the relation raised to the sum of those exponents is empty. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Assertion	relexpnul	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( dom ( 𝑅 ↑𝑟 𝑁 ) ∩ ran ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		coeq0	⊢ ( ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( dom ( 𝑅 ↑𝑟 𝑁 ) ∩ ran ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ )
2		simplr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → Rel 𝑅 )
3		simprl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
4		simprr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
5	2 3 4	relexpaddd	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
6	5	eqeq1d	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ ) )
7	1 6	bitr3id	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( dom ( 𝑅 ↑𝑟 𝑁 ) ∩ ran ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ ) )