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		simprl	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to N \in ℕ_{0}$
3		simprr	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to M \in ℕ_{0}$
4		simpll	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to R \in V$
5		simplr	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to Rel R$
6	5	a1d	$⊢ ((R \in V \land Rel R) \land (N \in ℕ_{0} \land M \in ℕ_{0})) \to (N + M = 1 \to Rel R)$
7		relexpaddg	$⊢ (N \in ℕ_{0} \land (M \in ℕ_{0} \land R \in V \land (N + M = 1 \to Rel R))) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
8	2 3 4 6 7	syl13anc	$⊢ ((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)$
9	8	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)$
10	1 9	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)$