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

Theorem isdrngd 18696
Description: Properties that determine a division ring. 𝐼 (reciprocal) is normally dependent on 𝑥 i.e. read it as 𝐼(𝑥)." (Contributed by NM, 2-Aug-2013.)
Hypotheses
Ref Expression
isdrngd.b (𝜑𝐵 = (Base‘𝑅))
isdrngd.t (𝜑· = (.r𝑅))
isdrngd.z (𝜑0 = (0g𝑅))
isdrngd.u (𝜑1 = (1r𝑅))
isdrngd.r (𝜑𝑅 ∈ Ring)
isdrngd.n ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ (𝑦𝐵𝑦0 )) → (𝑥 · 𝑦) ≠ 0 )
isdrngd.o (𝜑10 )
isdrngd.i ((𝜑 ∧ (𝑥𝐵𝑥0 )) → 𝐼𝐵)
isdrngd.j ((𝜑 ∧ (𝑥𝐵𝑥0 )) → 𝐼0 )
isdrngd.k ((𝜑 ∧ (𝑥𝐵𝑥0 )) → (𝐼 · 𝑥) = 1 )
Assertion
Ref Expression
isdrngd (𝜑𝑅 ∈ DivRing)
Distinct variable groups:   𝑥,𝑦, 0   𝑥, 1 ,𝑦   𝑥,𝐵,𝑦   𝑦,𝐼   𝑥,𝑅,𝑦   𝜑,𝑥,𝑦   𝑥, · ,𝑦
Allowed substitution hint:   𝐼(𝑥)

Proof of Theorem isdrngd
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 isdrngd.r . . 3 (𝜑𝑅 ∈ Ring)
2 difss 3717 . . . . . 6 (𝐵 ∖ { 0 }) ⊆ 𝐵
3 isdrngd.b . . . . . 6 (𝜑𝐵 = (Base‘𝑅))
42, 3syl5sseq 3634 . . . . 5 (𝜑 → (𝐵 ∖ { 0 }) ⊆ (Base‘𝑅))
5 eqid 2621 . . . . . 6 ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))
6 eqid 2621 . . . . . . 7 (mulGrp‘𝑅) = (mulGrp‘𝑅)
7 eqid 2621 . . . . . . 7 (Base‘𝑅) = (Base‘𝑅)
86, 7mgpbas 18419 . . . . . 6 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
95, 8ressbas2 15855 . . . . 5 ((𝐵 ∖ { 0 }) ⊆ (Base‘𝑅) → (𝐵 ∖ { 0 }) = (Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))))
104, 9syl 17 . . . 4 (𝜑 → (𝐵 ∖ { 0 }) = (Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))))
11 isdrngd.t . . . . 5 (𝜑· = (.r𝑅))
12 fvex 6160 . . . . . . 7 (Base‘𝑅) ∈ V
133, 12syl6eqel 2706 . . . . . 6 (𝜑𝐵 ∈ V)
14 difexg 4770 . . . . . 6 (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈ V)
15 eqid 2621 . . . . . . . 8 (.r𝑅) = (.r𝑅)
166, 15mgpplusg 18417 . . . . . . 7 (.r𝑅) = (+g‘(mulGrp‘𝑅))
175, 16ressplusg 15917 . . . . . 6 ((𝐵 ∖ { 0 }) ∈ V → (.r𝑅) = (+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))))
1813, 14, 173syl 18 . . . . 5 (𝜑 → (.r𝑅) = (+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))))
1911, 18eqtrd 2655 . . . 4 (𝜑· = (+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))))
20 eldifsn 4289 . . . . 5 (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥𝐵𝑥0 ))
21 eldifsn 4289 . . . . . 6 (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦𝐵𝑦0 ))
227, 15ringcl 18485 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r𝑅)𝑦) ∈ (Base‘𝑅))
231, 22syl3an1 1356 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r𝑅)𝑦) ∈ (Base‘𝑅))
24233expib 1265 . . . . . . . . . . 11 (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r𝑅)𝑦) ∈ (Base‘𝑅)))
253eleq2d 2684 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝑅)))
263eleq2d 2684 . . . . . . . . . . . 12 (𝜑 → (𝑦𝐵𝑦 ∈ (Base‘𝑅)))
2725, 26anbi12d 746 . . . . . . . . . . 11 (𝜑 → ((𝑥𝐵𝑦𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))))
2811oveqd 6624 . . . . . . . . . . . 12 (𝜑 → (𝑥 · 𝑦) = (𝑥(.r𝑅)𝑦))
2928, 3eleq12d 2692 . . . . . . . . . . 11 (𝜑 → ((𝑥 · 𝑦) ∈ 𝐵 ↔ (𝑥(.r𝑅)𝑦) ∈ (Base‘𝑅)))
3024, 27, 293imtr4d 283 . . . . . . . . . 10 (𝜑 → ((𝑥𝐵𝑦𝐵) → (𝑥 · 𝑦) ∈ 𝐵))
31303impib 1259 . . . . . . . . 9 ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 · 𝑦) ∈ 𝐵)
32313adant2r 1318 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ 𝑦𝐵) → (𝑥 · 𝑦) ∈ 𝐵)
33323adant3r 1320 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ (𝑦𝐵𝑦0 )) → (𝑥 · 𝑦) ∈ 𝐵)
34 isdrngd.n . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ (𝑦𝐵𝑦0 )) → (𝑥 · 𝑦) ≠ 0 )
35 eldifsn 4289 . . . . . . 7 ((𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥 · 𝑦) ∈ 𝐵 ∧ (𝑥 · 𝑦) ≠ 0 ))
3633, 34, 35sylanbrc 697 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ (𝑦𝐵𝑦0 )) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }))
3721, 36syl3an3b 1361 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑥0 ) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }))
3820, 37syl3an2b 1360 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }))
39 eldifi 3712 . . . . . 6 (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥𝐵)
40 eldifi 3712 . . . . . 6 (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦𝐵)
41 eldifi 3712 . . . . . 6 (𝑧 ∈ (𝐵 ∖ { 0 }) → 𝑧𝐵)
4239, 40, 413anim123i 1245 . . . . 5 ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 })) → (𝑥𝐵𝑦𝐵𝑧𝐵))
437, 15ringass 18488 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r𝑅)𝑦)(.r𝑅)𝑧) = (𝑥(.r𝑅)(𝑦(.r𝑅)𝑧)))
4443ex 450 . . . . . . . 8 (𝑅 ∈ Ring → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r𝑅)𝑦)(.r𝑅)𝑧) = (𝑥(.r𝑅)(𝑦(.r𝑅)𝑧))))
451, 44syl 17 . . . . . . 7 (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r𝑅)𝑦)(.r𝑅)𝑧) = (𝑥(.r𝑅)(𝑦(.r𝑅)𝑧))))
463eleq2d 2684 . . . . . . . 8 (𝜑 → (𝑧𝐵𝑧 ∈ (Base‘𝑅)))
4725, 26, 463anbi123d 1396 . . . . . . 7 (𝜑 → ((𝑥𝐵𝑦𝐵𝑧𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))))
48 eqidd 2622 . . . . . . . . 9 (𝜑𝑧 = 𝑧)
4911, 28, 48oveq123d 6628 . . . . . . . 8 (𝜑 → ((𝑥 · 𝑦) · 𝑧) = ((𝑥(.r𝑅)𝑦)(.r𝑅)𝑧))
50 eqidd 2622 . . . . . . . . 9 (𝜑𝑥 = 𝑥)
5111oveqd 6624 . . . . . . . . 9 (𝜑 → (𝑦 · 𝑧) = (𝑦(.r𝑅)𝑧))
5211, 50, 51oveq123d 6628 . . . . . . . 8 (𝜑 → (𝑥 · (𝑦 · 𝑧)) = (𝑥(.r𝑅)(𝑦(.r𝑅)𝑧)))
5349, 52eqeq12d 2636 . . . . . . 7 (𝜑 → (((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥(.r𝑅)𝑦)(.r𝑅)𝑧) = (𝑥(.r𝑅)(𝑦(.r𝑅)𝑧))))
5445, 47, 533imtr4d 283 . . . . . 6 (𝜑 → ((𝑥𝐵𝑦𝐵𝑧𝐵) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))))
5554imp 445 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
5642, 55sylan2 491 . . . 4 ((𝜑 ∧ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 }))) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
57 eqid 2621 . . . . . . . 8 (1r𝑅) = (1r𝑅)
587, 57ringidcl 18492 . . . . . . 7 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
591, 58syl 17 . . . . . 6 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
60 isdrngd.u . . . . . 6 (𝜑1 = (1r𝑅))
6159, 60, 33eltr4d 2713 . . . . 5 (𝜑1𝐵)
62 isdrngd.o . . . . 5 (𝜑10 )
63 eldifsn 4289 . . . . 5 ( 1 ∈ (𝐵 ∖ { 0 }) ↔ ( 1𝐵10 ))
6461, 62, 63sylanbrc 697 . . . 4 (𝜑1 ∈ (𝐵 ∖ { 0 }))
657, 15, 57ringlidm 18495 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) → ((1r𝑅)(.r𝑅)𝑥) = 𝑥)
6665ex 450 . . . . . . . . 9 (𝑅 ∈ Ring → (𝑥 ∈ (Base‘𝑅) → ((1r𝑅)(.r𝑅)𝑥) = 𝑥))
671, 66syl 17 . . . . . . . 8 (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((1r𝑅)(.r𝑅)𝑥) = 𝑥))
6811, 60, 50oveq123d 6628 . . . . . . . . 9 (𝜑 → ( 1 · 𝑥) = ((1r𝑅)(.r𝑅)𝑥))
6968eqeq1d 2623 . . . . . . . 8 (𝜑 → (( 1 · 𝑥) = 𝑥 ↔ ((1r𝑅)(.r𝑅)𝑥) = 𝑥))
7067, 25, 693imtr4d 283 . . . . . . 7 (𝜑 → (𝑥𝐵 → ( 1 · 𝑥) = 𝑥))
7170imp 445 . . . . . 6 ((𝜑𝑥𝐵) → ( 1 · 𝑥) = 𝑥)
7271adantrr 752 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑥0 )) → ( 1 · 𝑥) = 𝑥)
7320, 72sylan2b 492 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ { 0 })) → ( 1 · 𝑥) = 𝑥)
74 isdrngd.i . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑥0 )) → 𝐼𝐵)
75 isdrngd.j . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑥0 )) → 𝐼0 )
76 eldifsn 4289 . . . . . 6 (𝐼 ∈ (𝐵 ∖ { 0 }) ↔ (𝐼𝐵𝐼0 ))
7774, 75, 76sylanbrc 697 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑥0 )) → 𝐼 ∈ (𝐵 ∖ { 0 }))
7820, 77sylan2b 492 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ { 0 })) → 𝐼 ∈ (𝐵 ∖ { 0 }))
79 isdrngd.k . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑥0 )) → (𝐼 · 𝑥) = 1 )
8020, 79sylan2b 492 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ { 0 })) → (𝐼 · 𝑥) = 1 )
8110, 19, 38, 56, 64, 73, 78, 80isgrpd 17368 . . 3 (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp)
82 isdrngd.z . . . . . . . 8 (𝜑0 = (0g𝑅))
8382sneqd 4162 . . . . . . 7 (𝜑 → { 0 } = {(0g𝑅)})
843, 83difeq12d 3709 . . . . . 6 (𝜑 → (𝐵 ∖ { 0 }) = ((Base‘𝑅) ∖ {(0g𝑅)}))
8584oveq2d 6623 . . . . 5 (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) = ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})))
8685eleq1d 2683 . . . 4 (𝜑 → (((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp ↔ ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})) ∈ Grp))
8786anbi2d 739 . . 3 (𝜑 → ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp) ↔ (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})) ∈ Grp)))
881, 81, 87mpbi2and 955 . 2 (𝜑 → (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})) ∈ Grp))
89 eqid 2621 . . 3 (0g𝑅) = (0g𝑅)
90 eqid 2621 . . 3 ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})) = ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)}))
917, 89, 90isdrng2 18681 . 2 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s ((Base‘𝑅) ∖ {(0g𝑅)})) ∈ Grp))
9288, 91sylibr 224 1 (𝜑𝑅 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  Vcvv 3186  cdif 3553  wss 3556  {csn 4150  cfv 5849  (class class class)co 6607  Basecbs 15784  s cress 15785  +gcplusg 15865  .rcmulr 15866  0gc0g 16024  Grpcgrp 17346  mulGrpcmgp 18413  1rcur 18425  Ringcrg 18471  DivRingcdr 18671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-tpos 7300  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-0g 16026  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-grp 17349  df-minusg 17350  df-mgp 18414  df-ur 18426  df-ring 18473  df-oppr 18547  df-dvdsr 18565  df-unit 18566  df-invr 18596  df-dvr 18607  df-drng 18673
This theorem is referenced by:  isdrngrd  18697  cndrng  19697  erngdvlem4  35780
  Copyright terms: Public domain W3C validator