Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erngdv Structured version   Visualization version   GIF version

Theorem erngdv 38995
Description: An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
Hypotheses
Ref Expression
ernggrp.h 𝐻 = (LHyp‘𝐾)
ernggrp.d 𝐷 = ((EDRing‘𝐾)‘𝑊)
Assertion
Ref Expression
erngdv ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 ∈ DivRing)

Proof of Theorem erngdv
Dummy variables 𝑓 𝑠 𝑎 𝑏 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2740 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 ernggrp.h . . 3 𝐻 = (LHyp‘𝐾)
3 eqid 2740 . . 3 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
41, 2, 3cdlemftr0 38570 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ∃𝑓 ∈ ((LTrn‘𝐾)‘𝑊)𝑓 ≠ ( I ↾ (Base‘𝐾)))
5 ernggrp.d . . 3 𝐷 = ((EDRing‘𝐾)‘𝑊)
6 eqid 2740 . . 3 ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
7 eqid 2740 . . 3 (𝑎 ∈ ((TEndo‘𝐾)‘𝑊), 𝑏 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑎𝑓) ∘ (𝑏𝑓)))) = (𝑎 ∈ ((TEndo‘𝐾)‘𝑊), 𝑏 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑎𝑓) ∘ (𝑏𝑓))))
8 eqid 2740 . . 3 (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))
9 eqid 2740 . . 3 (𝑎 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑎𝑓))) = (𝑎 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑎𝑓)))
10 eqid 2740 . . 3 (𝑎 ∈ ((TEndo‘𝐾)‘𝑊), 𝑏 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑎𝑏)) = (𝑎 ∈ ((TEndo‘𝐾)‘𝑊), 𝑏 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑎𝑏))
11 eqid 2740 . . 3 (join‘𝐾) = (join‘𝐾)
12 eqid 2740 . . 3 (meet‘𝐾) = (meet‘𝐾)
13 eqid 2740 . . 3 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
14 eqid 2740 . . 3 ((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊)
15 eqid 2740 . . 3 ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓))))) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))
16 eqid 2740 . . 3 ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏)))) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏))))
17 eqid 2740 . . 3 (𝑧 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑏 ∈ ((LTrn‘𝐾)‘𝑊)((𝑏 ≠ ( I ↾ (Base‘𝐾)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘(𝑠𝑓)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘𝑔)) → (𝑧‘((oc‘𝐾)‘𝑊)) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏)))))) = (𝑧 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑏 ∈ ((LTrn‘𝐾)‘𝑊)((𝑏 ≠ ( I ↾ (Base‘𝐾)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘(𝑠𝑓)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘𝑔)) → (𝑧‘((oc‘𝐾)‘𝑊)) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏))))))
18 eqid 2740 . . 3 (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ if((𝑠𝑓) = 𝑓, 𝑔, (𝑧 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑏 ∈ ((LTrn‘𝐾)‘𝑊)((𝑏 ≠ ( I ↾ (Base‘𝐾)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘(𝑠𝑓)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘𝑔)) → (𝑧‘((oc‘𝐾)‘𝑊)) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏)))))))) = (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ if((𝑠𝑓) = 𝑓, 𝑔, (𝑧 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑏 ∈ ((LTrn‘𝐾)‘𝑊)((𝑏 ≠ ( I ↾ (Base‘𝐾)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘(𝑠𝑓)) ∧ (((trL‘𝐾)‘𝑊)‘𝑏) ≠ (((trL‘𝐾)‘𝑊)‘𝑔)) → (𝑧‘((oc‘𝐾)‘𝑊)) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))(meet‘𝐾)(((((oc‘𝐾)‘𝑊)(join‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑏))(meet‘𝐾)((𝑓‘((oc‘𝐾)‘𝑊))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑏(𝑠𝑓)))))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(𝑔𝑏))))))))
192, 5, 1, 3, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18erngdvlem4 38993 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑓 ≠ ( I ↾ (Base‘𝐾)))) → 𝐷 ∈ DivRing)
204, 19rexlimddv 3222 1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐷 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1542  wcel 2110  wne 2945  wral 3066  ifcif 4465  cmpt 5162   I cid 5488  ccnv 5588  cres 5591  ccom 5593  cfv 6431  crio 7225  (class class class)co 7269  cmpo 7271  Basecbs 16902  occoc 16960  joincjn 18019  meetcmee 18020  DivRingcdr 19981  HLchlt 37352  LHypclh 37986  LTrncltrn 38103  trLctrl 38160  TEndoctendo 38754  EDRingcedring 38755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-cnex 10920  ax-resscn 10921  ax-1cn 10922  ax-icn 10923  ax-addcl 10924  ax-addrcl 10925  ax-mulcl 10926  ax-mulrcl 10927  ax-mulcom 10928  ax-addass 10929  ax-mulass 10930  ax-distr 10931  ax-i2m1 10932  ax-1ne0 10933  ax-1rid 10934  ax-rnegex 10935  ax-rrecex 10936  ax-cnre 10937  ax-pre-lttri 10938  ax-pre-lttrn 10939  ax-pre-ltadd 10940  ax-pre-mulgt0 10941  ax-riotaBAD 36955
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-iun 4932  df-iin 4933  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7702  df-1st 7818  df-2nd 7819  df-tpos 8027  df-undef 8074  df-frecs 8082  df-wrecs 8113  df-recs 8187  df-rdg 8226  df-1o 8282  df-er 8473  df-map 8592  df-en 8709  df-dom 8710  df-sdom 8711  df-fin 8712  df-pnf 11004  df-mnf 11005  df-xr 11006  df-ltxr 11007  df-le 11008  df-sub 11199  df-neg 11200  df-nn 11966  df-2 12028  df-3 12029  df-n0 12226  df-z 12312  df-uz 12574  df-fz 13231  df-struct 16838  df-sets 16855  df-slot 16873  df-ndx 16885  df-base 16903  df-ress 16932  df-plusg 16965  df-mulr 16966  df-0g 17142  df-proset 18003  df-poset 18021  df-plt 18038  df-lub 18054  df-glb 18055  df-join 18056  df-meet 18057  df-p0 18133  df-p1 18134  df-lat 18140  df-clat 18207  df-mgm 18316  df-sgrp 18365  df-mnd 18376  df-grp 18570  df-minusg 18571  df-mgp 19711  df-ur 19728  df-ring 19775  df-oppr 19852  df-dvdsr 19873  df-unit 19874  df-invr 19904  df-dvr 19915  df-drng 19983  df-oposet 37178  df-ol 37180  df-oml 37181  df-covers 37268  df-ats 37269  df-atl 37300  df-cvlat 37324  df-hlat 37353  df-llines 37500  df-lplanes 37501  df-lvols 37502  df-lines 37503  df-psubsp 37505  df-pmap 37506  df-padd 37798  df-lhyp 37990  df-laut 37991  df-ldil 38106  df-ltrn 38107  df-trl 38161  df-tendo 38757  df-edring 38759
This theorem is referenced by:  erng1r  38997  dvalveclem  39027  dvhvaddass  39099  tendoinvcl  39106  tendolinv  39107  tendorinv  39108  dvhgrp  39109  dvhlveclem  39110  cdlemn4  39200  hlhildrng  39958
  Copyright terms: Public domain W3C validator