Metamath Proof Explorer

Theorem lmodfopne

Description: The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008) (Revised by AV, 2-Oct-2021)

Ref Expression
Hypotheses lmodfopne.t ⊢ · = ( ·sf ‘ 𝑊 )
lmodfopne.a ⊢ + = ( +𝑓 ‘ 𝑊 )
lmodfopne.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodfopne.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lmodfopne.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lmodfopne.0 ⊢ 0 = ( 0g ‘ 𝑆 )
lmodfopne.1 ⊢ 1 = ( 1r ‘ 𝑆 )
Assertion lmodfopne ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) → + ≠ · )

Proof

Step Hyp Ref Expression
1 lmodfopne.t ⊢ · = ( ·sf ‘ 𝑊 )
2 lmodfopne.a ⊢ + = ( +𝑓 ‘ 𝑊 )
3 lmodfopne.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lmodfopne.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5 lmodfopne.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 lmodfopne.0 ⊢ 0 = ( 0g ‘ 𝑆 )
7 lmodfopne.1 ⊢ 1 = ( 1r ‘ 𝑆 )
8 1 2 3 4 5 6 7 lmodfopnelem2 ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) )
9 simpl ⊢ ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → 0 ∈ 𝑉 )
10 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
11 3 10 lmod0vcl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
12 11 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
13 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
14 3 13 2 plusfval ⊢ ( ( 0 ∈ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) → ( 0 + ( 0g ‘ 𝑊 ) ) = ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
15 14 eqcomd ⊢ ( ( 0 ∈ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) → ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 0 + ( 0g ‘ 𝑊 ) ) )
16 9 12 15 syl2anr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 0 + ( 0g ‘ 𝑊 ) ) )
17 oveq ⊢ ( + = · → ( 0 + ( 0g ‘ 𝑊 ) ) = ( 0 · ( 0g ‘ 𝑊 ) ) )
18 17 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 + ( 0g ‘ 𝑊 ) ) = ( 0 · ( 0g ‘ 𝑊 ) ) )
19 16 18 eqtrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 0 · ( 0g ‘ 𝑊 ) ) )
20 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
21 20 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → 𝑊 ∈ Grp )
22 3 13 10 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ 0 ∈ 𝑉 ) → ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 0 )
23 21 9 22 syl2an ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 0 )
24 4 5 6 lmod0cl ⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝐾 )
25 24 11 jca ⊢ ( 𝑊 ∈ LMod → ( 0 ∈ 𝐾 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) )
26 25 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝐾 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) )
27 26 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 ∈ 𝐾 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) )
28 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
29 3 4 5 1 28 scafval ⊢ ( ( 0 ∈ 𝐾 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) → ( 0 · ( 0g ‘ 𝑊 ) ) = ( 0 ( ·𝑠 ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
30 27 29 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 · ( 0g ‘ 𝑊 ) ) = ( 0 ( ·𝑠 ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
31 24 ancli ⊢ ( 𝑊 ∈ LMod → ( 𝑊 ∈ LMod ∧ 0 ∈ 𝐾 ) )
32 31 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 𝑊 ∈ LMod ∧ 0 ∈ 𝐾 ) )
33 32 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 𝑊 ∈ LMod ∧ 0 ∈ 𝐾 ) )
34 4 28 5 10 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ 0 ∈ 𝐾 ) → ( 0 ( ·𝑠 ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
35 33 34 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 ( ·𝑠 ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
36 simpr ⊢ ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → 1 ∈ 𝑉 )
37 3 13 10 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ 1 ∈ 𝑉 ) → ( 1 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 1 )
38 21 36 37 syl2an ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 1 )
39 4 5 7 lmod1cl ⊢ ( 𝑊 ∈ LMod → 1 ∈ 𝐾 )
40 39 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → 1 ∈ 𝐾 )
41 3 4 5 1 28 scafval ⊢ ( ( 1 ∈ 𝐾 ∧ 1 ∈ 𝑉 ) → ( 1 · 1 ) = ( 1 ( ·𝑠 ‘ 𝑊 ) 1 ) )
42 40 36 41 syl2an ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 · 1 ) = ( 1 ( ·𝑠 ‘ 𝑊 ) 1 ) )
43 3 4 28 7 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 1 ∈ 𝑉 ) → ( 1 ( ·𝑠 ‘ 𝑊 ) 1 ) = 1 )
44 43 ad2ant2rl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 ( ·𝑠 ‘ 𝑊 ) 1 ) = 1 )
45 42 44 eqtrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 · 1 ) = 1 )
46 oveq ⊢ ( + = · → ( 1 + 1 ) = ( 1 · 1 ) )
47 46 eqcomd ⊢ ( + = · → ( 1 · 1 ) = ( 1 + 1 ) )
48 47 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 · 1 ) = ( 1 + 1 ) )
49 36 36 jca ⊢ ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → ( 1 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) )
50 49 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) )
51 3 13 2 plusfval ⊢ ( ( 1 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → ( 1 + 1 ) = ( 1 ( +g ‘ 𝑊 ) 1 ) )
52 50 51 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 + 1 ) = ( 1 ( +g ‘ 𝑊 ) 1 ) )
53 48 52 eqtrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 · 1 ) = ( 1 ( +g ‘ 𝑊 ) 1 ) )
54 38 45 53 3eqtr2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 1 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 1 ( +g ‘ 𝑊 ) 1 ) )
55 21 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → 𝑊 ∈ Grp )
56 12 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
57 36 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → 1 ∈ 𝑉 )
58 3 13 grplcan ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 0g ‘ 𝑊 ) ∈ 𝑉 ∧ 1 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( ( 1 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 1 ( +g ‘ 𝑊 ) 1 ) ↔ ( 0g ‘ 𝑊 ) = 1 ) )
59 55 56 57 57 58 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( ( 1 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 1 ( +g ‘ 𝑊 ) 1 ) ↔ ( 0g ‘ 𝑊 ) = 1 ) )
60 54 59 mpbid ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0g ‘ 𝑊 ) = 1 )
61 30 35 60 3eqtrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → ( 0 · ( 0g ‘ 𝑊 ) ) = 1 )
62 19 23 61 3eqtr3rd ⊢ ( ( ( 𝑊 ∈ LMod ∧ + = · ) ∧ ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) → 1 = 0 )
63 8 62 mpdan ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → 1 = 0 )
64 63 ex ⊢ ( 𝑊 ∈ LMod → ( + = · → 1 = 0 ) )
65 64 necon3d ⊢ ( 𝑊 ∈ LMod → ( 1 ≠ 0 → + ≠ · ) )
66 65 imp ⊢ ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) → + ≠ · )