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	⊢ · = ( ·sf ‘ 𝑊 )
	clmopfne.a	⊢ + = ( +𝑓 ‘ 𝑊 )
Assertion	clmopfne	⊢ ( 𝑊 ∈ ℂMod → + ≠ · )

Proof

Step	Hyp	Ref	Expression
1		clmopfne.t	⊢ · = ( ·sf ‘ 𝑊 )
2		clmopfne.a	⊢ + = ( +𝑓 ‘ 𝑊 )
3		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
4		ax-1ne0	⊢ 1 ≠ 0
5	4	a1i	⊢ ( 𝑊 ∈ ℂMod → 1 ≠ 0 )
6		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7	6	clm1	⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
8	6	clm0	⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9	5 7 8	3netr3d	⊢ ( 𝑊 ∈ ℂMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
12		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
13		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
14	1 2 10 6 11 12 13	lmodfopne	⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → + ≠ · )
15	3 9 14	syl2anc	⊢ ( 𝑊 ∈ ℂMod → + ≠ · )