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	|- ( ph -> Rel R )
	relexpaddd.2	|- ( ph -> N e. NN0 )
	relexpaddd.3	|- ( ph -> M e. NN0 )
Assertion	relexpaddd	|- ( ph -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )

Proof

Step	Hyp	Ref	Expression
1		relexpaddd.1	|- ( ph -> Rel R )
2		relexpaddd.2	|- ( ph -> N e. NN0 )
3		relexpaddd.3	|- ( ph -> M e. NN0 )
4	2	adantr	|- ( ( ph /\ R e. _V ) -> N e. NN0 )
5	3	adantr	|- ( ( ph /\ R e. _V ) -> M e. NN0 )
6		simpr	|- ( ( ph /\ R e. _V ) -> R e. _V )
7	1	a1d	|- ( ph -> ( ( N + M ) = 1 -> Rel R ) )
8	7	adantr	|- ( ( ph /\ R e. _V ) -> ( ( N + M ) = 1 -> Rel R ) )
9		relexpaddg	|- ( ( N e. NN0 /\ ( M e. NN0 /\ R e. _V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
10	4 5 6 8 9	syl13anc	|- ( ( ph /\ R e. _V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
11	10	ex	|- ( ph -> ( R e. _V -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
12		co01	|- ( (/) o. (/) ) = (/)
13		reldmrelexp	|- Rel dom ^r
14	13	ovprc1	|- ( -. R e. _V -> ( R ^r N ) = (/) )
15	13	ovprc1	|- ( -. R e. _V -> ( R ^r M ) = (/) )
16	14 15	coeq12d	|- ( -. R e. _V -> ( ( R ^r N ) o. ( R ^r M ) ) = ( (/) o. (/) ) )
17	13	ovprc1	|- ( -. R e. _V -> ( R ^r ( N + M ) ) = (/) )
18	12 16 17	3eqtr4a	|- ( -. R e. _V -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
19	11 18	pm2.61d1	|- ( ph -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )