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		simprl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
3		simprr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑀 ∈ ℕ0 )
4		simpll	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑅 ∈ 𝑉 )
5		simplr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → Rel 𝑅 )
6	5	a1d	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) )
7		relexpaddg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
8	2 3 4 6 7	syl13anc	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
9	8	eqeq1d	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ ) )
10	1 9	bitr3id	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( dom ( 𝑅 ↑𝑟 𝑁 ) ∩ ran ( 𝑅 ↑𝑟 𝑀 ) ) = ∅ ↔ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ ) )