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 ⊢ · = ( ·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 → + ≠ · )