MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idsrngd Structured version   Visualization version   GIF version

Theorem idsrngd 19609
Description: A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.)
Hypotheses
Ref Expression
idsrngd.k 𝐵 = (Base‘𝑅)
idsrngd.c = (*𝑟𝑅)
idsrngd.r (𝜑𝑅 ∈ CRing)
idsrngd.i ((𝜑𝑥𝐵) → ( 𝑥) = 𝑥)
Assertion
Ref Expression
idsrngd (𝜑𝑅 ∈ *-Ring)
Distinct variable groups:   𝑥,   𝑥,𝐵   𝑥,𝑅   𝜑,𝑥

Proof of Theorem idsrngd
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idsrngd.k . . 3 𝐵 = (Base‘𝑅)
21a1i 11 . 2 (𝜑𝐵 = (Base‘𝑅))
3 eqidd 2821 . 2 (𝜑 → (+g𝑅) = (+g𝑅))
4 eqidd 2821 . 2 (𝜑 → (.r𝑅) = (.r𝑅))
5 idsrngd.c . . 3 = (*𝑟𝑅)
65a1i 11 . 2 (𝜑 = (*𝑟𝑅))
7 idsrngd.r . . 3 (𝜑𝑅 ∈ CRing)
8 crngring 19287 . . 3 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
97, 8syl 17 . 2 (𝜑𝑅 ∈ Ring)
10 idsrngd.i . . . . . 6 ((𝜑𝑥𝐵) → ( 𝑥) = 𝑥)
1110ralrimiva 3169 . . . . 5 (𝜑 → ∀𝑥𝐵 ( 𝑥) = 𝑥)
1211adantr 483 . . . 4 ((𝜑𝑎𝐵) → ∀𝑥𝐵 ( 𝑥) = 𝑥)
13 simpr 487 . . . . 5 ((𝜑𝑎𝐵) → 𝑎𝐵)
14 simpr 487 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑥 = 𝑎) → 𝑥 = 𝑎)
1514fveq2d 6650 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑥 = 𝑎) → ( 𝑥) = ( 𝑎))
1615, 14eqeq12d 2836 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑥 = 𝑎) → (( 𝑥) = 𝑥 ↔ ( 𝑎) = 𝑎))
1713, 16rspcdv 3594 . . . 4 ((𝜑𝑎𝐵) → (∀𝑥𝐵 ( 𝑥) = 𝑥 → ( 𝑎) = 𝑎))
1812, 17mpd 15 . . 3 ((𝜑𝑎𝐵) → ( 𝑎) = 𝑎)
1918, 13eqeltrd 2911 . 2 ((𝜑𝑎𝐵) → ( 𝑎) ∈ 𝐵)
2011adantr 483 . . . . 5 ((𝜑𝑏𝐵) → ∀𝑥𝐵 ( 𝑥) = 𝑥)
21203adant2 1127 . . . 4 ((𝜑𝑎𝐵𝑏𝐵) → ∀𝑥𝐵 ( 𝑥) = 𝑥)
22 ringgrp 19281 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
239, 22syl 17 . . . . . 6 (𝜑𝑅 ∈ Grp)
24 eqid 2820 . . . . . . 7 (+g𝑅) = (+g𝑅)
251, 24grpcl 18090 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝑎𝐵𝑏𝐵) → (𝑎(+g𝑅)𝑏) ∈ 𝐵)
2623, 25syl3an1 1159 . . . . 5 ((𝜑𝑎𝐵𝑏𝐵) → (𝑎(+g𝑅)𝑏) ∈ 𝐵)
27 simpr 487 . . . . . . 7 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(+g𝑅)𝑏)) → 𝑥 = (𝑎(+g𝑅)𝑏))
2827fveq2d 6650 . . . . . 6 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(+g𝑅)𝑏)) → ( 𝑥) = ( ‘(𝑎(+g𝑅)𝑏)))
2928, 27eqeq12d 2836 . . . . 5 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(+g𝑅)𝑏)) → (( 𝑥) = 𝑥 ↔ ( ‘(𝑎(+g𝑅)𝑏)) = (𝑎(+g𝑅)𝑏)))
3026, 29rspcdv 3594 . . . 4 ((𝜑𝑎𝐵𝑏𝐵) → (∀𝑥𝐵 ( 𝑥) = 𝑥 → ( ‘(𝑎(+g𝑅)𝑏)) = (𝑎(+g𝑅)𝑏)))
3121, 30mpd 15 . . 3 ((𝜑𝑎𝐵𝑏𝐵) → ( ‘(𝑎(+g𝑅)𝑏)) = (𝑎(+g𝑅)𝑏))
32183adant3 1128 . . . 4 ((𝜑𝑎𝐵𝑏𝐵) → ( 𝑎) = 𝑎)
33 simpr 487 . . . . . . 7 ((𝜑𝑏𝐵) → 𝑏𝐵)
34 simpr 487 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑥 = 𝑏) → 𝑥 = 𝑏)
3534fveq2d 6650 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑥 = 𝑏) → ( 𝑥) = ( 𝑏))
3635, 34eqeq12d 2836 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑥 = 𝑏) → (( 𝑥) = 𝑥 ↔ ( 𝑏) = 𝑏))
3733, 36rspcdv 3594 . . . . . 6 ((𝜑𝑏𝐵) → (∀𝑥𝐵 ( 𝑥) = 𝑥 → ( 𝑏) = 𝑏))
3820, 37mpd 15 . . . . 5 ((𝜑𝑏𝐵) → ( 𝑏) = 𝑏)
39383adant2 1127 . . . 4 ((𝜑𝑎𝐵𝑏𝐵) → ( 𝑏) = 𝑏)
4032, 39oveq12d 7151 . . 3 ((𝜑𝑎𝐵𝑏𝐵) → (( 𝑎)(+g𝑅)( 𝑏)) = (𝑎(+g𝑅)𝑏))
4131, 40eqtr4d 2858 . 2 ((𝜑𝑎𝐵𝑏𝐵) → ( ‘(𝑎(+g𝑅)𝑏)) = (( 𝑎)(+g𝑅)( 𝑏)))
42 eqid 2820 . . . . 5 (.r𝑅) = (.r𝑅)
431, 42crngcom 19291 . . . 4 ((𝑅 ∈ CRing ∧ 𝑎𝐵𝑏𝐵) → (𝑎(.r𝑅)𝑏) = (𝑏(.r𝑅)𝑎))
447, 43syl3an1 1159 . . 3 ((𝜑𝑎𝐵𝑏𝐵) → (𝑎(.r𝑅)𝑏) = (𝑏(.r𝑅)𝑎))
451, 42ringcl 19290 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝑎𝐵𝑏𝐵) → (𝑎(.r𝑅)𝑏) ∈ 𝐵)
469, 45syl3an1 1159 . . . . 5 ((𝜑𝑎𝐵𝑏𝐵) → (𝑎(.r𝑅)𝑏) ∈ 𝐵)
47 simpr 487 . . . . . . 7 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(.r𝑅)𝑏)) → 𝑥 = (𝑎(.r𝑅)𝑏))
4847fveq2d 6650 . . . . . 6 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(.r𝑅)𝑏)) → ( 𝑥) = ( ‘(𝑎(.r𝑅)𝑏)))
4948, 47eqeq12d 2836 . . . . 5 (((𝜑𝑎𝐵𝑏𝐵) ∧ 𝑥 = (𝑎(.r𝑅)𝑏)) → (( 𝑥) = 𝑥 ↔ ( ‘(𝑎(.r𝑅)𝑏)) = (𝑎(.r𝑅)𝑏)))
5046, 49rspcdv 3594 . . . 4 ((𝜑𝑎𝐵𝑏𝐵) → (∀𝑥𝐵 ( 𝑥) = 𝑥 → ( ‘(𝑎(.r𝑅)𝑏)) = (𝑎(.r𝑅)𝑏)))
5121, 50mpd 15 . . 3 ((𝜑𝑎𝐵𝑏𝐵) → ( ‘(𝑎(.r𝑅)𝑏)) = (𝑎(.r𝑅)𝑏))
5239, 32oveq12d 7151 . . 3 ((𝜑𝑎𝐵𝑏𝐵) → (( 𝑏)(.r𝑅)( 𝑎)) = (𝑏(.r𝑅)𝑎))
5344, 51, 523eqtr4d 2865 . 2 ((𝜑𝑎𝐵𝑏𝐵) → ( ‘(𝑎(.r𝑅)𝑏)) = (( 𝑏)(.r𝑅)( 𝑎)))
5418fveq2d 6650 . . 3 ((𝜑𝑎𝐵) → ( ‘( 𝑎)) = ( 𝑎))
5554, 18eqtrd 2855 . 2 ((𝜑𝑎𝐵) → ( ‘( 𝑎)) = 𝑎)
562, 3, 4, 6, 9, 19, 41, 53, 55issrngd 19608 1 (𝜑𝑅 ∈ *-Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083   = wceq 1537  wcel 2114  wral 3125  cfv 6331  (class class class)co 7133  Basecbs 16462  +gcplusg 16544  .rcmulr 16545  *𝑟cstv 16546  Grpcgrp 18082  Ringcrg 19276  CRingccrg 19277  *-Ringcsr 19591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-tpos 7870  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-nn 11617  df-2 11679  df-3 11680  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-plusg 16557  df-mulr 16558  df-0g 16694  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-mhm 17935  df-grp 18085  df-ghm 18335  df-cmn 18887  df-mgp 19219  df-ur 19231  df-ring 19278  df-cring 19279  df-oppr 19352  df-rnghom 19446  df-staf 19592  df-srng 19593
This theorem is referenced by:  recrng  20741  frlmphl  20901
  Copyright terms: Public domain W3C validator