ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lmodfopne GIF version

Theorem lmodfopne 13825
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.)
Hypotheses
Ref Expression
lmodfopne.t · = ( ·sf𝑊)
lmodfopne.a + = (+𝑓𝑊)
lmodfopne.v 𝑉 = (Base‘𝑊)
lmodfopne.s 𝑆 = (Scalar‘𝑊)
lmodfopne.k 𝐾 = (Base‘𝑆)
lmodfopne.0 0 = (0g𝑆)
lmodfopne.1 1 = (1r𝑆)
Assertion
Ref Expression
lmodfopne ((𝑊 ∈ LMod ∧ 10 ) → +· )

Proof of Theorem lmodfopne
StepHypRef Expression
1 lmodfopne.t . . . . . 6 · = ( ·sf𝑊)
2 lmodfopne.a . . . . . 6 + = (+𝑓𝑊)
3 lmodfopne.v . . . . . 6 𝑉 = (Base‘𝑊)
4 lmodfopne.s . . . . . 6 𝑆 = (Scalar‘𝑊)
5 lmodfopne.k . . . . . 6 𝐾 = (Base‘𝑆)
6 lmodfopne.0 . . . . . 6 0 = (0g𝑆)
7 lmodfopne.1 . . . . . 6 1 = (1r𝑆)
81, 2, 3, 4, 5, 6, 7lmodfopnelem2 13824 . . . . 5 ((𝑊 ∈ LMod ∧ + = · ) → ( 0𝑉1𝑉))
9 simpll 527 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 𝑊 ∈ LMod)
10 simpl 109 . . . . . . . . 9 (( 0𝑉1𝑉) → 0𝑉)
1110adantl 277 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 0𝑉)
12 eqid 2193 . . . . . . . . . 10 (0g𝑊) = (0g𝑊)
133, 12lmod0vcl 13816 . . . . . . . . 9 (𝑊 ∈ LMod → (0g𝑊) ∈ 𝑉)
1413ad2antrr 488 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → (0g𝑊) ∈ 𝑉)
15 eqid 2193 . . . . . . . . . 10 (+g𝑊) = (+g𝑊)
163, 15, 2plusfvalg 12949 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ 0𝑉 ∧ (0g𝑊) ∈ 𝑉) → ( 0 + (0g𝑊)) = ( 0 (+g𝑊)(0g𝑊)))
1716eqcomd 2199 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 0𝑉 ∧ (0g𝑊) ∈ 𝑉) → ( 0 (+g𝑊)(0g𝑊)) = ( 0 + (0g𝑊)))
189, 11, 14, 17syl3anc 1249 . . . . . . 7 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 (+g𝑊)(0g𝑊)) = ( 0 + (0g𝑊)))
19 oveq 5925 . . . . . . . 8 ( + = · → ( 0 + (0g𝑊)) = ( 0 · (0g𝑊)))
2019ad2antlr 489 . . . . . . 7 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 + (0g𝑊)) = ( 0 · (0g𝑊)))
2118, 20eqtrd 2226 . . . . . 6 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 (+g𝑊)(0g𝑊)) = ( 0 · (0g𝑊)))
22 lmodgrp 13793 . . . . . . . 8 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2322adantr 276 . . . . . . 7 ((𝑊 ∈ LMod ∧ + = · ) → 𝑊 ∈ Grp)
243, 15, 12grprid 13107 . . . . . . 7 ((𝑊 ∈ Grp ∧ 0𝑉) → ( 0 (+g𝑊)(0g𝑊)) = 0 )
2523, 10, 24syl2an 289 . . . . . 6 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 (+g𝑊)(0g𝑊)) = 0 )
264, 5, 6lmod0cl 13813 . . . . . . . . 9 (𝑊 ∈ LMod → 0𝐾)
2726ad2antrr 488 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 0𝐾)
28 eqid 2193 . . . . . . . . 9 ( ·𝑠𝑊) = ( ·𝑠𝑊)
293, 4, 5, 1, 28scafvalg 13806 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 0𝐾 ∧ (0g𝑊) ∈ 𝑉) → ( 0 · (0g𝑊)) = ( 0 ( ·𝑠𝑊)(0g𝑊)))
309, 27, 14, 29syl3anc 1249 . . . . . . 7 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 · (0g𝑊)) = ( 0 ( ·𝑠𝑊)(0g𝑊)))
3126ancli 323 . . . . . . . . 9 (𝑊 ∈ LMod → (𝑊 ∈ LMod ∧ 0𝐾))
3231ad2antrr 488 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → (𝑊 ∈ LMod ∧ 0𝐾))
334, 28, 5, 12lmodvs0 13821 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 0𝐾) → ( 0 ( ·𝑠𝑊)(0g𝑊)) = (0g𝑊))
3432, 33syl 14 . . . . . . 7 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 ( ·𝑠𝑊)(0g𝑊)) = (0g𝑊))
35 simpr 110 . . . . . . . . . 10 (( 0𝑉1𝑉) → 1𝑉)
363, 15, 12grprid 13107 . . . . . . . . . 10 ((𝑊 ∈ Grp ∧ 1𝑉) → ( 1 (+g𝑊)(0g𝑊)) = 1 )
3723, 35, 36syl2an 289 . . . . . . . . 9 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 (+g𝑊)(0g𝑊)) = 1 )
384, 5, 7lmod1cl 13814 . . . . . . . . . . . 12 (𝑊 ∈ LMod → 1𝐾)
3938ad2antrr 488 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 1𝐾)
4035adantl 277 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 1𝑉)
413, 4, 5, 1, 28scafvalg 13806 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ 1𝐾1𝑉) → ( 1 · 1 ) = ( 1 ( ·𝑠𝑊) 1 ))
429, 39, 40, 41syl3anc 1249 . . . . . . . . . 10 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 · 1 ) = ( 1 ( ·𝑠𝑊) 1 ))
433, 4, 28, 7lmodvs1 13815 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ 1𝑉) → ( 1 ( ·𝑠𝑊) 1 ) = 1 )
4443ad2ant2rl 511 . . . . . . . . . 10 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 ( ·𝑠𝑊) 1 ) = 1 )
4542, 44eqtrd 2226 . . . . . . . . 9 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 · 1 ) = 1 )
46 oveq 5925 . . . . . . . . . . . 12 ( + = · → ( 1 + 1 ) = ( 1 · 1 ))
4746eqcomd 2199 . . . . . . . . . . 11 ( + = · → ( 1 · 1 ) = ( 1 + 1 ))
4847ad2antlr 489 . . . . . . . . . 10 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 · 1 ) = ( 1 + 1 ))
493, 15, 2plusfvalg 12949 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ 1𝑉1𝑉) → ( 1 + 1 ) = ( 1 (+g𝑊) 1 ))
509, 40, 40, 49syl3anc 1249 . . . . . . . . . 10 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 + 1 ) = ( 1 (+g𝑊) 1 ))
5148, 50eqtrd 2226 . . . . . . . . 9 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 · 1 ) = ( 1 (+g𝑊) 1 ))
5237, 45, 513eqtr2d 2232 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 1 (+g𝑊)(0g𝑊)) = ( 1 (+g𝑊) 1 ))
5322ad2antrr 488 . . . . . . . . 9 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 𝑊 ∈ Grp)
543, 15grplcan 13137 . . . . . . . . 9 ((𝑊 ∈ Grp ∧ ((0g𝑊) ∈ 𝑉1𝑉1𝑉)) → (( 1 (+g𝑊)(0g𝑊)) = ( 1 (+g𝑊) 1 ) ↔ (0g𝑊) = 1 ))
5553, 14, 40, 40, 54syl13anc 1251 . . . . . . . 8 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → (( 1 (+g𝑊)(0g𝑊)) = ( 1 (+g𝑊) 1 ) ↔ (0g𝑊) = 1 ))
5652, 55mpbid 147 . . . . . . 7 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → (0g𝑊) = 1 )
5730, 34, 563eqtrd 2230 . . . . . 6 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → ( 0 · (0g𝑊)) = 1 )
5821, 25, 573eqtr3rd 2235 . . . . 5 (((𝑊 ∈ LMod ∧ + = · ) ∧ ( 0𝑉1𝑉)) → 1 = 0 )
598, 58mpdan 421 . . . 4 ((𝑊 ∈ LMod ∧ + = · ) → 1 = 0 )
6059ex 115 . . 3 (𝑊 ∈ LMod → ( + = ·1 = 0 ))
6160necon3d 2408 . 2 (𝑊 ∈ LMod → ( 10+· ))
6261imp 124 1 ((𝑊 ∈ LMod ∧ 10 ) → +· )
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 980   = wceq 1364  wcel 2164  wne 2364  cfv 5255  (class class class)co 5919  Basecbs 12621  +gcplusg 12698  Scalarcsca 12701   ·𝑠 cvsca 12702  0gc0g 12870  +𝑓cplusf 12939  Grpcgrp 13075  1rcur 13458  LModclmod 13786   ·sf cscaf 13787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4145  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-pre-ltirr 7986  ax-pre-ltadd 7990
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2987  df-csb 3082  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-iun 3915  df-br 4031  df-opab 4092  df-mpt 4093  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-1st 6195  df-2nd 6196  df-pnf 8058  df-mnf 8059  df-ltxr 8061  df-inn 8985  df-2 9043  df-3 9044  df-4 9045  df-5 9046  df-6 9047  df-ndx 12624  df-slot 12625  df-base 12627  df-sets 12628  df-plusg 12711  df-mulr 12712  df-sca 12714  df-vsca 12715  df-0g 12872  df-plusf 12941  df-mgm 12942  df-sgrp 12988  df-mnd 13001  df-grp 13078  df-minusg 13079  df-mgp 13420  df-ur 13459  df-ring 13497  df-lmod 13788  df-scaf 13789
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator