Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngoueqz Structured version   Visualization version   GIF version

Theorem rngoueqz 36797
Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20300 instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.)
Hypotheses
Ref Expression
uznzr.1 𝐺 = (1st𝑅)
uznzr.2 𝐻 = (2nd𝑅)
uznzr.3 𝑍 = (GId‘𝐺)
uznzr.4 𝑈 = (GId‘𝐻)
uznzr.5 𝑋 = ran 𝐺
Assertion
Ref Expression
rngoueqz (𝑅 ∈ RingOps → (𝑋 ≈ 1o𝑈 = 𝑍))

Proof of Theorem rngoueqz
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 uznzr.1 . . . 4 𝐺 = (1st𝑅)
2 uznzr.5 . . . 4 𝑋 = ran 𝐺
3 uznzr.3 . . . 4 𝑍 = (GId‘𝐺)
41, 2, 3rngo0cl 36776 . . 3 (𝑅 ∈ RingOps → 𝑍𝑋)
5 en1eqsn 9271 . . . . . 6 ((𝑍𝑋𝑋 ≈ 1o) → 𝑋 = {𝑍})
61rneqi 5935 . . . . . . . 8 ran 𝐺 = ran (1st𝑅)
7 uznzr.2 . . . . . . . 8 𝐻 = (2nd𝑅)
8 uznzr.4 . . . . . . . 8 𝑈 = (GId‘𝐻)
96, 7, 8rngo1cl 36796 . . . . . . 7 (𝑅 ∈ RingOps → 𝑈 ∈ ran 𝐺)
10 eleq2 2823 . . . . . . . . . 10 (𝑋 = {𝑍} → (𝑈𝑋𝑈 ∈ {𝑍}))
1110biimpd 228 . . . . . . . . 9 (𝑋 = {𝑍} → (𝑈𝑋𝑈 ∈ {𝑍}))
12 elsni 4645 . . . . . . . . 9 (𝑈 ∈ {𝑍} → 𝑈 = 𝑍)
1311, 12syl6com 37 . . . . . . . 8 (𝑈𝑋 → (𝑋 = {𝑍} → 𝑈 = 𝑍))
142eqcomi 2742 . . . . . . . 8 ran 𝐺 = 𝑋
1513, 14eleq2s 2852 . . . . . . 7 (𝑈 ∈ ran 𝐺 → (𝑋 = {𝑍} → 𝑈 = 𝑍))
169, 15syl 17 . . . . . 6 (𝑅 ∈ RingOps → (𝑋 = {𝑍} → 𝑈 = 𝑍))
175, 16syl5com 31 . . . . 5 ((𝑍𝑋𝑋 ≈ 1o) → (𝑅 ∈ RingOps → 𝑈 = 𝑍))
1817ex 414 . . . 4 (𝑍𝑋 → (𝑋 ≈ 1o → (𝑅 ∈ RingOps → 𝑈 = 𝑍)))
1918com23 86 . . 3 (𝑍𝑋 → (𝑅 ∈ RingOps → (𝑋 ≈ 1o𝑈 = 𝑍)))
204, 19mpcom 38 . 2 (𝑅 ∈ RingOps → (𝑋 ≈ 1o𝑈 = 𝑍))
211, 2rngone0 36768 . . 3 (𝑅 ∈ RingOps → 𝑋 ≠ ∅)
22 oveq2 7414 . . . . . 6 (𝑈 = 𝑍 → (𝑥𝐻𝑈) = (𝑥𝐻𝑍))
2322ralrimivw 3151 . . . . 5 (𝑈 = 𝑍 → ∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍))
243, 2, 1, 7rngorz 36780 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑥𝑋) → (𝑥𝐻𝑍) = 𝑍)
2524ralrimiva 3147 . . . . . 6 (𝑅 ∈ RingOps → ∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍)
262, 6eqtri 2761 . . . . . . . . 9 𝑋 = ran (1st𝑅)
277, 26, 8rngoridm 36795 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑥𝑋) → (𝑥𝐻𝑈) = 𝑥)
2827ralrimiva 3147 . . . . . . 7 (𝑅 ∈ RingOps → ∀𝑥𝑋 (𝑥𝐻𝑈) = 𝑥)
29 r19.26 3112 . . . . . . . . . 10 (∀𝑥𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ↔ (∀𝑥𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)))
30 r19.26 3112 . . . . . . . . . . . 12 (∀𝑥𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) ↔ (∀𝑥𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍))
31 eqtr 2756 . . . . . . . . . . . . . . . . . 18 ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → 𝑥 = (𝑥𝐻𝑍))
32 eqtr 2756 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = (𝑥𝐻𝑍) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍)
3332ex 414 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍𝑥 = 𝑍))
3431, 33syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → ((𝑥𝐻𝑍) = 𝑍𝑥 = 𝑍))
3534ex 414 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑥𝐻𝑈) → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍𝑥 = 𝑍)))
3635eqcoms 2741 . . . . . . . . . . . . . . 15 ((𝑥𝐻𝑈) = 𝑥 → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍𝑥 = 𝑍)))
3736imp31 419 . . . . . . . . . . . . . 14 ((((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍)
3837ralimi 3084 . . . . . . . . . . . . 13 (∀𝑥𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → ∀𝑥𝑋 𝑥 = 𝑍)
39 eqsn 4832 . . . . . . . . . . . . . . 15 (𝑋 ≠ ∅ → (𝑋 = {𝑍} ↔ ∀𝑥𝑋 𝑥 = 𝑍))
40 ensn1g 9016 . . . . . . . . . . . . . . . . 17 (𝑍𝑋 → {𝑍} ≈ 1o)
414, 40syl 17 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → {𝑍} ≈ 1o)
42 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑋 = {𝑍} → (𝑋 ≈ 1o ↔ {𝑍} ≈ 1o))
4341, 42imbitrrid 245 . . . . . . . . . . . . . . 15 (𝑋 = {𝑍} → (𝑅 ∈ RingOps → 𝑋 ≈ 1o))
4439, 43syl6bir 254 . . . . . . . . . . . . . 14 (𝑋 ≠ ∅ → (∀𝑥𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → 𝑋 ≈ 1o)))
4544com3l 89 . . . . . . . . . . . . 13 (∀𝑥𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))
4638, 45syl 17 . . . . . . . . . . . 12 (∀𝑥𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))
4730, 46sylbir 234 . . . . . . . . . . 11 ((∀𝑥𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))
4847ex 414 . . . . . . . . . 10 (∀𝑥𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))
4929, 48sylbir 234 . . . . . . . . 9 ((∀𝑥𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))
5049ex 414 . . . . . . . 8 (∀𝑥𝑋 (𝑥𝐻𝑈) = 𝑥 → (∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))))
5150com24 95 . . . . . . 7 (∀𝑥𝑋 (𝑥𝐻𝑈) = 𝑥 → (𝑅 ∈ RingOps → (∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))))
5228, 51mpcom 38 . . . . . 6 (𝑅 ∈ RingOps → (∀𝑥𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))
5325, 52mpd 15 . . . . 5 (𝑅 ∈ RingOps → (∀𝑥𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))
5423, 53syl5com 31 . . . 4 (𝑈 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))
5554com13 88 . . 3 (𝑋 ≠ ∅ → (𝑅 ∈ RingOps → (𝑈 = 𝑍𝑋 ≈ 1o)))
5621, 55mpcom 38 . 2 (𝑅 ∈ RingOps → (𝑈 = 𝑍𝑋 ≈ 1o))
5720, 56impbid 211 1 (𝑅 ∈ RingOps → (𝑋 ≈ 1o𝑈 = 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2941  wral 3062  c0 4322  {csn 4628   class class class wbr 5148  ran crn 5677  cfv 6541  (class class class)co 7406  1st c1st 7970  2nd c2nd 7971  1oc1o 8456  cen 8933  GIdcgi 29731  RingOpscrngo 36751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-1st 7972  df-2nd 7973  df-1o 8463  df-en 8937  df-grpo 29734  df-gid 29735  df-ablo 29786  df-ass 36700  df-exid 36702  df-mgmOLD 36706  df-sgrOLD 36718  df-mndo 36724  df-rngo 36752
This theorem is referenced by:  dvrunz  36811  isdmn3  36931
  Copyright terms: Public domain W3C validator