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 
|- .x. = ( .sf ` W )
lmodfopne.a 
|- .+ = ( +f ` W )
lmodfopne.v 
|- V = ( Base ` W )
lmodfopne.s 
|- S = ( Scalar ` W )
lmodfopne.k 
|- K = ( Base ` S )
lmodfopne.0 
|- .0. = ( 0g ` S )
lmodfopne.1 
|- .1. = ( 1r ` S )
Assertion lmodfopne 
|- ( ( W e. LMod /\ .1. =/= .0. ) -> .+ =/= .x. )

Proof

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