| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lmodnegadd.v |
|- V = ( Base ` W ) |
| 2 |
|
lmodnegadd.p |
|- .+ = ( +g ` W ) |
| 3 |
|
lmodnegadd.t |
|- .x. = ( .s ` W ) |
| 4 |
|
lmodnegadd.n |
|- N = ( invg ` W ) |
| 5 |
|
lmodnegadd.r |
|- R = ( Scalar ` W ) |
| 6 |
|
lmodnegadd.k |
|- K = ( Base ` R ) |
| 7 |
|
lmodnegadd.i |
|- I = ( invg ` R ) |
| 8 |
|
lmodnegadd.w |
|- ( ph -> W e. LMod ) |
| 9 |
|
lmodnegadd.a |
|- ( ph -> A e. K ) |
| 10 |
|
lmodnegadd.b |
|- ( ph -> B e. K ) |
| 11 |
|
lmodnegadd.x |
|- ( ph -> X e. V ) |
| 12 |
|
lmodnegadd.y |
|- ( ph -> Y e. V ) |
| 13 |
|
lmodabl |
|- ( W e. LMod -> W e. Abel ) |
| 14 |
8 13
|
syl |
|- ( ph -> W e. Abel ) |
| 15 |
1 5 3 6
|
lmodvscl |
|- ( ( W e. LMod /\ A e. K /\ X e. V ) -> ( A .x. X ) e. V ) |
| 16 |
8 9 11 15
|
syl3anc |
|- ( ph -> ( A .x. X ) e. V ) |
| 17 |
1 5 3 6
|
lmodvscl |
|- ( ( W e. LMod /\ B e. K /\ Y e. V ) -> ( B .x. Y ) e. V ) |
| 18 |
8 10 12 17
|
syl3anc |
|- ( ph -> ( B .x. Y ) e. V ) |
| 19 |
1 2 4
|
ablinvadd |
|- ( ( W e. Abel /\ ( A .x. X ) e. V /\ ( B .x. Y ) e. V ) -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) ) |
| 20 |
14 16 18 19
|
syl3anc |
|- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) ) |
| 21 |
1 5 3 4 6 7 8 11 9
|
lmodvsneg |
|- ( ph -> ( N ` ( A .x. X ) ) = ( ( I ` A ) .x. X ) ) |
| 22 |
1 5 3 4 6 7 8 12 10
|
lmodvsneg |
|- ( ph -> ( N ` ( B .x. Y ) ) = ( ( I ` B ) .x. Y ) ) |
| 23 |
21 22
|
oveq12d |
|- ( ph -> ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) ) |
| 24 |
20 23
|
eqtrd |
|- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) ) |