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 ) ) ) )