Step |
Hyp |
Ref |
Expression |
1 |
|
phlsrng.f |
|- F = ( Scalar ` W ) |
2 |
|
phllmhm.h |
|- ., = ( .i ` W ) |
3 |
|
phllmhm.v |
|- V = ( Base ` W ) |
4 |
|
ipdir.g |
|- .+ = ( +g ` W ) |
5 |
|
ipdir.p |
|- .+^ = ( +g ` F ) |
6 |
|
eqid |
|- ( x e. V |-> ( x ., C ) ) = ( x e. V |-> ( x ., C ) ) |
7 |
1 2 3 6
|
phllmhm |
|- ( ( W e. PreHil /\ C e. V ) -> ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) ) |
8 |
7
|
3ad2antr3 |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) ) |
9 |
|
lmghm |
|- ( ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) -> ( x e. V |-> ( x ., C ) ) e. ( W GrpHom ( ringLMod ` F ) ) ) |
10 |
8 9
|
syl |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( x e. V |-> ( x ., C ) ) e. ( W GrpHom ( ringLMod ` F ) ) ) |
11 |
|
simpr1 |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> A e. V ) |
12 |
|
simpr2 |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> B e. V ) |
13 |
|
rlmplusg |
|- ( +g ` F ) = ( +g ` ( ringLMod ` F ) ) |
14 |
5 13
|
eqtri |
|- .+^ = ( +g ` ( ringLMod ` F ) ) |
15 |
3 4 14
|
ghmlin |
|- ( ( ( x e. V |-> ( x ., C ) ) e. ( W GrpHom ( ringLMod ` F ) ) /\ A e. V /\ B e. V ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .+ B ) ) = ( ( ( x e. V |-> ( x ., C ) ) ` A ) .+^ ( ( x e. V |-> ( x ., C ) ) ` B ) ) ) |
16 |
10 11 12 15
|
syl3anc |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .+ B ) ) = ( ( ( x e. V |-> ( x ., C ) ) ` A ) .+^ ( ( x e. V |-> ( x ., C ) ) ` B ) ) ) |
17 |
|
phllmod |
|- ( W e. PreHil -> W e. LMod ) |
18 |
3 4
|
lmodvacl |
|- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .+ B ) e. V ) |
19 |
17 18
|
syl3an1 |
|- ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A .+ B ) e. V ) |
20 |
19
|
3adant3r3 |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A .+ B ) e. V ) |
21 |
|
oveq1 |
|- ( x = ( A .+ B ) -> ( x ., C ) = ( ( A .+ B ) ., C ) ) |
22 |
|
ovex |
|- ( x ., C ) e. _V |
23 |
21 6 22
|
fvmpt3i |
|- ( ( A .+ B ) e. V -> ( ( x e. V |-> ( x ., C ) ) ` ( A .+ B ) ) = ( ( A .+ B ) ., C ) ) |
24 |
20 23
|
syl |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .+ B ) ) = ( ( A .+ B ) ., C ) ) |
25 |
|
oveq1 |
|- ( x = A -> ( x ., C ) = ( A ., C ) ) |
26 |
25 6 22
|
fvmpt3i |
|- ( A e. V -> ( ( x e. V |-> ( x ., C ) ) ` A ) = ( A ., C ) ) |
27 |
11 26
|
syl |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` A ) = ( A ., C ) ) |
28 |
|
oveq1 |
|- ( x = B -> ( x ., C ) = ( B ., C ) ) |
29 |
28 6 22
|
fvmpt3i |
|- ( B e. V -> ( ( x e. V |-> ( x ., C ) ) ` B ) = ( B ., C ) ) |
30 |
12 29
|
syl |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` B ) = ( B ., C ) ) |
31 |
27 30
|
oveq12d |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( x e. V |-> ( x ., C ) ) ` A ) .+^ ( ( x e. V |-> ( x ., C ) ) ` B ) ) = ( ( A ., C ) .+^ ( B ., C ) ) ) |
32 |
16 24 31
|
3eqtr3d |
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) .+^ ( B ., C ) ) ) |