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. )