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	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	clmopfne.a	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(W\right)$$
Assertion	clmopfne	$$⊢W\in \mathrm{CMod}\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}$$

Proof

Step	Hyp	Ref	Expression
1		clmopfne.t	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
2		clmopfne.a	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(W\right)$$
3		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
4		ax-1ne0	$$⊢1\ne 0$$
5	4	a1i	$$⊢W\in \mathrm{CMod}\to 1\ne 0$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7	6	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_{\mathrm{Scalar}\left(W\right)}$$
8	6	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
9	5 7 8	3netr3d	$$⊢W\in \mathrm{CMod}\to 1_{\mathrm{Scalar}\left(W\right)}\ne 0_{\mathrm{Scalar}\left(W\right)}$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
12		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
13		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
14	1 2 10 6 11 12 13	lmodfopne	$$⊢\left(W\in \mathrm{LMod}\wedge 1_{\mathrm{Scalar}\left(W\right)}\ne 0_{\mathrm{Scalar}\left(W\right)}\right)\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}$$
15	3 9 14	syl2anc	$$⊢W\in \mathrm{CMod}\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}$$