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

Theorem unitrrg 13747
Description: Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
Hypotheses
Ref Expression
unitrrg.e 𝐸 = (RLReg‘𝑅)
unitrrg.u 𝑈 = (Unit‘𝑅)
Assertion
Ref Expression
unitrrg (𝑅 ∈ Ring → 𝑈𝐸)

Proof of Theorem unitrrg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2193 . . . . . 6 (Base‘𝑅) = (Base‘𝑅)
21a1i 9 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → (Base‘𝑅) = (Base‘𝑅))
3 unitrrg.u . . . . . 6 𝑈 = (Unit‘𝑅)
43a1i 9 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → 𝑈 = (Unit‘𝑅))
5 ringsrg 13527 . . . . . 6 (𝑅 ∈ Ring → 𝑅 ∈ SRing)
65adantr 276 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → 𝑅 ∈ SRing)
7 simpr 110 . . . . 5 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → 𝑥𝑈)
82, 4, 6, 7unitcld 13588 . . . 4 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → 𝑥 ∈ (Base‘𝑅))
9 oveq2 5918 . . . . . 6 ((𝑥(.r𝑅)𝑦) = (0g𝑅) → (((invr𝑅)‘𝑥)(.r𝑅)(𝑥(.r𝑅)𝑦)) = (((invr𝑅)‘𝑥)(.r𝑅)(0g𝑅)))
10 eqid 2193 . . . . . . . . . . 11 (invr𝑅) = (invr𝑅)
11 eqid 2193 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
12 eqid 2193 . . . . . . . . . . 11 (1r𝑅) = (1r𝑅)
133, 10, 11, 12unitlinv 13606 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → (((invr𝑅)‘𝑥)(.r𝑅)𝑥) = (1r𝑅))
1413adantr 276 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr𝑅)‘𝑥)(.r𝑅)𝑥) = (1r𝑅))
1514oveq1d 5925 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr𝑅)‘𝑥)(.r𝑅)𝑥)(.r𝑅)𝑦) = ((1r𝑅)(.r𝑅)𝑦))
16 simpll 527 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
173, 10, 1ringinvcl 13605 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → ((invr𝑅)‘𝑥) ∈ (Base‘𝑅))
1817adantr 276 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((invr𝑅)‘𝑥) ∈ (Base‘𝑅))
198adantr 276 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
20 simpr 110 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 ∈ (Base‘𝑅))
211, 11ringass 13496 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ (((invr𝑅)‘𝑥) ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → ((((invr𝑅)‘𝑥)(.r𝑅)𝑥)(.r𝑅)𝑦) = (((invr𝑅)‘𝑥)(.r𝑅)(𝑥(.r𝑅)𝑦)))
2216, 18, 19, 20, 21syl13anc 1251 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr𝑅)‘𝑥)(.r𝑅)𝑥)(.r𝑅)𝑦) = (((invr𝑅)‘𝑥)(.r𝑅)(𝑥(.r𝑅)𝑦)))
231, 11, 12ringlidm 13503 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → ((1r𝑅)(.r𝑅)𝑦) = 𝑦)
2423adantlr 477 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((1r𝑅)(.r𝑅)𝑦) = 𝑦)
2515, 22, 243eqtr3d 2234 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr𝑅)‘𝑥)(.r𝑅)(𝑥(.r𝑅)𝑦)) = 𝑦)
26 eqid 2193 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
271, 11, 26ringrz 13524 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ((invr𝑅)‘𝑥) ∈ (Base‘𝑅)) → (((invr𝑅)‘𝑥)(.r𝑅)(0g𝑅)) = (0g𝑅))
2816, 18, 27syl2anc 411 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr𝑅)‘𝑥)(.r𝑅)(0g𝑅)) = (0g𝑅))
2925, 28eqeq12d 2208 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr𝑅)‘𝑥)(.r𝑅)(𝑥(.r𝑅)𝑦)) = (((invr𝑅)‘𝑥)(.r𝑅)(0g𝑅)) ↔ 𝑦 = (0g𝑅)))
309, 29imbitrid 154 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑥𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r𝑅)𝑦) = (0g𝑅) → 𝑦 = (0g𝑅)))
3130ralrimiva 2567 . . . 4 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → 𝑦 = (0g𝑅)))
32 unitrrg.e . . . . 5 𝐸 = (RLReg‘𝑅)
3332, 1, 11, 26isrrg 13743 . . . 4 (𝑥𝐸 ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → 𝑦 = (0g𝑅))))
348, 31, 33sylanbrc 417 . . 3 ((𝑅 ∈ Ring ∧ 𝑥𝑈) → 𝑥𝐸)
3534ex 115 . 2 (𝑅 ∈ Ring → (𝑥𝑈𝑥𝐸))
3635ssrdv 3185 1 (𝑅 ∈ Ring → 𝑈𝐸)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1364  wcel 2164  wral 2472  wss 3153  cfv 5246  (class class class)co 5910  Basecbs 12608  .rcmulr 12686  0gc0g 12857  1rcur 13439  SRingcsrg 13443  Ringcrg 13476  Unitcui 13567  invrcinvr 13600  RLRegcrlreg 13735
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 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-addcom 7962  ax-addass 7964  ax-i2m1 7967  ax-0lt1 7968  ax-0id 7970  ax-rnegex 7971  ax-pre-ltirr 7974  ax-pre-lttrn 7976  ax-pre-ltadd 7978
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 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4322  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-tpos 6289  df-pnf 8046  df-mnf 8047  df-ltxr 8049  df-inn 8973  df-2 9031  df-3 9032  df-ndx 12611  df-slot 12612  df-base 12614  df-sets 12615  df-iress 12616  df-plusg 12698  df-mulr 12699  df-0g 12859  df-mgm 12929  df-sgrp 12975  df-mnd 12988  df-grp 13065  df-minusg 13066  df-cmn 13345  df-abl 13346  df-mgp 13401  df-ur 13440  df-srg 13444  df-ring 13478  df-oppr 13548  df-dvdsr 13569  df-unit 13570  df-invr 13601  df-rlreg 13738
This theorem is referenced by:  znrrg  14125
  Copyright terms: Public domain W3C validator