Metamath Proof Explorer

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	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to (dom (R ↑_{r} N) \cap ran (R ↑_{r} M) = \emptyset \leftrightarrow R ↑_{r} (N + M) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		coeq0	$⊢ (R ↑_{r} N) \circ (R ↑_{r} M) = \emptyset \leftrightarrow dom (R ↑_{r} N) \cap ran (R ↑_{r} M) = \emptyset$
2		simplr	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to Rel R$
3		simprl	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to N \in ℕ_{0}$
4		simprr	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to M \in ℕ_{0}$
5	2 3 4	relexpaddd	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
6	5	eqeq1d	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to ((R ↑_{r} N) \circ (R ↑_{r} M) = \emptyset \leftrightarrow R ↑_{r} (N + M) = \emptyset)$
7	1 6	bitr3id	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to (dom (R ↑_{r} N) \cap ran (R ↑_{r} M) = \emptyset \leftrightarrow R ↑_{r} (N + M) = \emptyset)$