This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmopfne

Description: The (functionalized) operations of addition and multiplication by a scalar of a subcomplex module cannot be identical. (Contributed by NM, 31-May-2008) (Revised by AV, 3-Oct-2021)

Ref Expression
Hypotheses clmopfne.t 
|- .x. = ( .sf ` W )
clmopfne.a 
|- .+ = ( +f ` W )
Assertion clmopfne 
|- ( W e. CMod -> .+ =/= .x. )

Proof

Step Hyp Ref Expression
1 clmopfne.t 
 |-  .x. = ( .sf ` W )
2 clmopfne.a 
 |-  .+ = ( +f ` W )
3 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
4 ax-1ne0 
 |-  1 =/= 0
5 4 a1i 
 |-  ( W e. CMod -> 1 =/= 0 )
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 6 clm1 
 |-  ( W e. CMod -> 1 = ( 1r ` ( Scalar ` W ) ) )
8 6 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
9 5 7 8 3netr3d 
 |-  ( W e. CMod -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
12 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
13 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
14 1 2 10 6 11 12 13 lmodfopne 
 |-  ( ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) -> .+ =/= .x. )
15 3 9 14 syl2anc 
 |-  ( W e. CMod -> .+ =/= .x. )