Metamath Proof Explorer

Theorem ercpbl

Description: Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypotheses ercpbl.r 
|- ( ph -> .~ Er V )
ercpbl.v 
|- ( ph -> V e. W )
ercpbl.f 
|- F = ( x e. V |-> [ x ] .~ )
ercpbl.c 
|- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )
ercpbl.e 
|- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )
Assertion ercpbl 
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )

Proof

Step Hyp Ref Expression
1 ercpbl.r 
 |-  ( ph -> .~ Er V )
2 ercpbl.v 
 |-  ( ph -> V e. W )
3 ercpbl.f 
 |-  F = ( x e. V |-> [ x ] .~ )
4 ercpbl.c 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )
5 ercpbl.e 
 |-  ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )
6 5 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )
7 1 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> .~ Er V )
8 2 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> V e. W )
9 simp2l 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> A e. V )
10 7 8 3 9 ercpbllem 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` A ) = ( F ` C ) <-> A .~ C ) )
11 simp2r 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> B e. V )
12 7 8 3 11 ercpbllem 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` B ) = ( F ` D ) <-> B .~ D ) )
13 10 12 anbi12d 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A .~ C /\ B .~ D ) ) )
14 4 caovclg 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) ) -> ( A .+ B ) e. V )
15 14 3adant3 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( A .+ B ) e. V )
16 7 8 3 15 ercpbllem 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) <-> ( A .+ B ) .~ ( C .+ D ) ) )
17 6 13 16 3imtr4d 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )