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 e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 coeq0 
 |-  ( ( ( R ^r N ) o. ( R ^r M ) ) = (/) <-> ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) )
2 simprl 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> N e. NN0 )
3 simprr 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> M e. NN0 )
4 simpll 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> R e. V )
5 simplr 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> Rel R )
6 5 a1d 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( N + M ) = 1 -> Rel R ) )
7 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 ) ) )
8 2 3 4 6 7 syl13anc 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
9 8 eqeq1d 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( ( R ^r N ) o. ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )
10 1 9 bitr3id 
 |-  ( ( ( R e. V /\ Rel R ) /\ ( N e. NN0 /\ M e. NN0 ) ) -> ( ( dom ( R ^r N ) i^i ran ( R ^r M ) ) = (/) <-> ( R ^r ( N + M ) ) = (/) ) )