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	⊢ ( 𝜑 → Rel 𝑅 )
	relexpaddd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	relexpaddd.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion	relexpaddd	⊢ ( 𝜑 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		relexpaddd.1	⊢ ( 𝜑 → Rel 𝑅 )
2		relexpaddd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		relexpaddd.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑁 ∈ ℕ0 )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑀 ∈ ℕ0 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
7	1	a1d	⊢ ( 𝜑 → ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) )
9		relexpaddg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ V ∧ ( ( 𝑁 + 𝑀 ) = 1 → Rel 𝑅 ) ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
10	4 5 6 8 9	syl13anc	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
11	10	ex	⊢ ( 𝜑 → ( 𝑅 ∈ V → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) )
12		co01	⊢ ( ∅ ∘ ∅ ) = ∅
13		reldmrelexp	⊢ Rel dom ↑𝑟
14	13	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑁 ) = ∅ )
15	13	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑀 ) = ∅ )
16	14 15	coeq12d	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ∅ ∘ ∅ ) )
17	13	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ∅ )
18	12 16 17	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
19	11 18	pm2.61d1	⊢ ( 𝜑 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )