Metamath Proof Explorer

Theorem clmvsubval

Description: Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 . (Contributed by NM, 31-Mar-2014) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvsubval.v 
|- V = ( Base ` W )
clmvsubval.p 
|- .+ = ( +g ` W )
clmvsubval.m 
|- .- = ( -g ` W )
clmvsubval.f 
|- F = ( Scalar ` W )
clmvsubval.s 
|- .x. = ( .s ` W )
Assertion clmvsubval 
|- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( -u 1 .x. B ) ) )

Proof

Step Hyp Ref Expression
1 clmvsubval.v 
 |-  V = ( Base ` W )
2 clmvsubval.p 
 |-  .+ = ( +g ` W )
3 clmvsubval.m 
 |-  .- = ( -g ` W )
4 clmvsubval.f 
 |-  F = ( Scalar ` W )
5 clmvsubval.s 
 |-  .x. = ( .s ` W )
6 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
7 eqid 
 |-  ( invg ` F ) = ( invg ` F )
8 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
9 1 2 3 4 5 7 8 lmodvsubval2 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. B ) ) )
10 6 9 syl3an1 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. B ) ) )
11 4 clm1 
 |-  ( W e. CMod -> 1 = ( 1r ` F ) )
12 11 eqcomd 
 |-  ( W e. CMod -> ( 1r ` F ) = 1 )
13 12 fveq2d 
 |-  ( W e. CMod -> ( ( invg ` F ) ` ( 1r ` F ) ) = ( ( invg ` F ) ` 1 ) )
14 4 clmring 
 |-  ( W e. CMod -> F e. Ring )
15 eqid 
 |-  ( Base ` F ) = ( Base ` F )
16 15 8 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) )
17 14 16 syl 
 |-  ( W e. CMod -> ( 1r ` F ) e. ( Base ` F ) )
18 11 17 eqeltrd 
 |-  ( W e. CMod -> 1 e. ( Base ` F ) )
19 4 15 clmneg 
 |-  ( ( W e. CMod /\ 1 e. ( Base ` F ) ) -> -u 1 = ( ( invg ` F ) ` 1 ) )
20 18 19 mpdan 
 |-  ( W e. CMod -> -u 1 = ( ( invg ` F ) ` 1 ) )
21 13 20 eqtr4d 
 |-  ( W e. CMod -> ( ( invg ` F ) ` ( 1r ` F ) ) = -u 1 )
22 21 3ad2ant1 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( ( invg ` F ) ` ( 1r ` F ) ) = -u 1 )
23 22 oveq1d 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. B ) = ( -u 1 .x. B ) )
24 23 oveq2d 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. B ) ) = ( A .+ ( -u 1 .x. B ) ) )
25 10 24 eqtrd 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( -u 1 .x. B ) ) )