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