| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cphipcj.h |
|- ., = ( .i ` W ) |
| 2 |
|
cphipcj.v |
|- V = ( Base ` W ) |
| 3 |
|
cphdir.P |
|- .+ = ( +g ` W ) |
| 4 |
|
cph2di.1 |
|- ( ph -> W e. CPreHil ) |
| 5 |
|
cph2di.2 |
|- ( ph -> A e. V ) |
| 6 |
|
cph2di.3 |
|- ( ph -> B e. V ) |
| 7 |
|
cph2di.4 |
|- ( ph -> C e. V ) |
| 8 |
|
cph2di.5 |
|- ( ph -> D e. V ) |
| 9 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 10 |
|
eqid |
|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) ) |
| 11 |
|
cphphl |
|- ( W e. CPreHil -> W e. PreHil ) |
| 12 |
4 11
|
syl |
|- ( ph -> W e. PreHil ) |
| 13 |
9 1 2 3 10 12 5 6 7 8
|
ip2di |
|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( +g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) ) |
| 14 |
|
cphclm |
|- ( W e. CPreHil -> W e. CMod ) |
| 15 |
9
|
clmadd |
|- ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) ) |
| 16 |
4 14 15
|
3syl |
|- ( ph -> + = ( +g ` ( Scalar ` W ) ) ) |
| 17 |
16
|
oveqd |
|- ( ph -> ( ( A ., C ) + ( B ., D ) ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ) |
| 18 |
16
|
oveqd |
|- ( ph -> ( ( A ., D ) + ( B ., C ) ) = ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) |
| 19 |
16 17 18
|
oveq123d |
|- ( ph -> ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( +g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) ) |
| 20 |
13 19
|
eqtr4d |
|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) ) |