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	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
		clmopfne.a	$⊢ \underset{˙}{+} = +_{𝑓} (W)$
	Assertion	clmopfne	$⊢ W \in CMod \to \underset{˙}{+} \neq \underset{˙}{\cdot}$

Proof

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