Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  drgext0gsca Structured version   Visualization version   GIF version

Theorem drgext0gsca 31424
Description: The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
Hypotheses
Ref Expression
drgext.b 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
drgext.1 (𝜑𝐸 ∈ DivRing)
drgext.2 (𝜑𝑈 ∈ (SubRing‘𝐸))
Assertion
Ref Expression
drgext0gsca (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))

Proof of Theorem drgext0gsca
StepHypRef Expression
1 drgext.1 . . . 4 (𝜑𝐸 ∈ DivRing)
2 drngring 19806 . . . 4 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
3 ringmnd 19604 . . . 4 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
41, 2, 33syl 18 . . 3 (𝜑𝐸 ∈ Mnd)
5 drgext.2 . . . 4 (𝜑𝑈 ∈ (SubRing‘𝐸))
6 subrgsubg 19838 . . . 4 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ∈ (SubGrp‘𝐸))
7 eqid 2739 . . . . 5 (0g𝐸) = (0g𝐸)
87subg0cl 18583 . . . 4 (𝑈 ∈ (SubGrp‘𝐸) → (0g𝐸) ∈ 𝑈)
95, 6, 83syl 18 . . 3 (𝜑 → (0g𝐸) ∈ 𝑈)
10 eqid 2739 . . . . 5 (Base‘𝐸) = (Base‘𝐸)
1110subrgss 19833 . . . 4 (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸))
125, 11syl 17 . . 3 (𝜑𝑈 ⊆ (Base‘𝐸))
13 eqid 2739 . . . 4 (𝐸s 𝑈) = (𝐸s 𝑈)
1413, 10, 7ress0g 18233 . . 3 ((𝐸 ∈ Mnd ∧ (0g𝐸) ∈ 𝑈𝑈 ⊆ (Base‘𝐸)) → (0g𝐸) = (0g‘(𝐸s 𝑈)))
154, 9, 12, 14syl3anc 1373 . 2 (𝜑 → (0g𝐸) = (0g‘(𝐸s 𝑈)))
16 drgext.b . . 3 𝐵 = ((subringAlg ‘𝐸)‘𝑈)
1716, 1, 5drgext0g 31422 . 2 (𝜑 → (0g𝐸) = (0g𝐵))
1816a1i 11 . . . 4 (𝜑𝐵 = ((subringAlg ‘𝐸)‘𝑈))
1918, 12srasca 20250 . . 3 (𝜑 → (𝐸s 𝑈) = (Scalar‘𝐵))
2019fveq2d 6742 . 2 (𝜑 → (0g‘(𝐸s 𝑈)) = (0g‘(Scalar‘𝐵)))
2115, 17, 203eqtr3d 2787 1 (𝜑 → (0g𝐵) = (0g‘(Scalar‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  wss 3883  cfv 6400  (class class class)co 7234  Basecbs 16792  s cress 16816  Scalarcsca 16837  0gc0g 16976  Mndcmnd 18205  SubGrpcsubg 18569  Ringcrg 19594  DivRingcdr 19799  SubRingcsubrg 19828  subringAlg csra 20237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-nn 11860  df-2 11922  df-3 11923  df-4 11924  df-5 11925  df-6 11926  df-7 11927  df-8 11928  df-sets 16749  df-slot 16767  df-ndx 16777  df-base 16793  df-ress 16817  df-plusg 16847  df-sca 16850  df-vsca 16851  df-ip 16852  df-0g 16978  df-mgm 18146  df-sgrp 18195  df-mnd 18206  df-grp 18400  df-subg 18572  df-ring 19596  df-drng 19801  df-subrg 19830  df-sra 20241
This theorem is referenced by:  fedgmullem2  31456
  Copyright terms: Public domain W3C validator