Metamath Proof Explorer

Theorem relexpaddd

Description: Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

		Ref	Expression
	Hypotheses	relexpaddd.1	$⊢ φ \to Rel R$
		relexpaddd.2	$⊢ φ \to N \in ℕ_{0}$
		relexpaddd.3	$⊢ φ \to M \in ℕ_{0}$
	Assertion	relexpaddd	$⊢ φ \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$

Proof

Step	Hyp	Ref	Expression
1		relexpaddd.1	$⊢ φ \to Rel R$
2		relexpaddd.2	$⊢ φ \to N \in ℕ_{0}$
3		relexpaddd.3	$⊢ φ \to M \in ℕ_{0}$
4	2	adantr	$⊢ (φ \land R \in V) \to N \in ℕ_{0}$
5	3	adantr	$⊢ (φ \land R \in V) \to M \in ℕ_{0}$
6		simpr	$⊢ (φ \land R \in V) \to R \in V$
7	1	a1d	$⊢ φ \to (N + M = 1 \to Rel R)$
8	7	adantr	$⊢ (φ \land R \in V) \to (N + M = 1 \to Rel R)$
9		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)$
10	4 5 6 8 9	syl13anc	$⊢ (φ \land R \in V) \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
11	10	ex	$⊢ φ \to (R \in V \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M))$
12		co01	$⊢ \emptyset \circ \emptyset = \emptyset$
13		reldmrelexp	$⊢ Rel dom ↑_{r}$
14	13	ovprc1	$⊢ \neg R \in V \to R ↑_{r} N = \emptyset$
15	13	ovprc1	$⊢ \neg R \in V \to R ↑_{r} M = \emptyset$
16	14 15	coeq12d	$⊢ \neg R \in V \to (R ↑_{r} N) \circ (R ↑_{r} M) = \emptyset \circ \emptyset$
17	13	ovprc1	$⊢ \neg R \in V \to R ↑_{r} (N + M) = \emptyset$
18	12 16 17	3eqtr4a	$⊢ \neg R \in V \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$
19	11 18	pm2.61d1	$⊢ φ \to (R ↑_{r} N) \circ (R ↑_{r} M) = R ↑_{r} (N + M)$