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

Theorem smprngopr 33981
 Description: A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
Hypotheses
Ref Expression
smprngpr.1 𝐺 = (1st𝑅)
smprngpr.2 𝐻 = (2nd𝑅)
smprngpr.3 𝑋 = ran 𝐺
smprngpr.4 𝑍 = (GId‘𝐺)
smprngpr.5 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
smprngopr ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)

Proof of Theorem smprngopr
Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1081 . 2 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ RingOps)
2 smprngpr.1 . . . . 5 𝐺 = (1st𝑅)
3 smprngpr.4 . . . . 5 𝑍 = (GId‘𝐺)
42, 30idl 33954 . . . 4 (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
543ad2ant1 1102 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (Idl‘𝑅))
6 smprngpr.2 . . . . . . . 8 𝐻 = (2nd𝑅)
7 smprngpr.3 . . . . . . . 8 𝑋 = ran 𝐺
8 smprngpr.5 . . . . . . . 8 𝑈 = (GId‘𝐻)
92, 6, 7, 3, 80rngo 33956 . . . . . . 7 (𝑅 ∈ RingOps → (𝑍 = 𝑈𝑋 = {𝑍}))
10 eqcom 2658 . . . . . . 7 (𝑈 = 𝑍𝑍 = 𝑈)
11 eqcom 2658 . . . . . . 7 ({𝑍} = 𝑋𝑋 = {𝑍})
129, 10, 113bitr4g 303 . . . . . 6 (𝑅 ∈ RingOps → (𝑈 = 𝑍 ↔ {𝑍} = 𝑋))
1312necon3bid 2867 . . . . 5 (𝑅 ∈ RingOps → (𝑈𝑍 ↔ {𝑍} ≠ 𝑋))
1413biimpa 500 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → {𝑍} ≠ 𝑋)
15143adant3 1101 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ≠ 𝑋)
16 df-pr 4213 . . . . . . . 8 {{𝑍}, 𝑋} = ({{𝑍}} ∪ {𝑋})
1716eqeq2i 2663 . . . . . . 7 ((Idl‘𝑅) = {{𝑍}, 𝑋} ↔ (Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}))
18 eleq2 2719 . . . . . . . . 9 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ ({{𝑍}} ∪ {𝑋})))
19 eleq2 2719 . . . . . . . . 9 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑗 ∈ (Idl‘𝑅) ↔ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})))
2018, 19anbi12d 747 . . . . . . . 8 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋}))))
21 elun 3786 . . . . . . . . . 10 (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}))
22 velsn 4226 . . . . . . . . . . 11 (𝑖 ∈ {{𝑍}} ↔ 𝑖 = {𝑍})
23 velsn 4226 . . . . . . . . . . 11 (𝑖 ∈ {𝑋} ↔ 𝑖 = 𝑋)
2422, 23orbi12i 542 . . . . . . . . . 10 ((𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
2521, 24bitri 264 . . . . . . . . 9 (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
26 elun 3786 . . . . . . . . . 10 (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}))
27 velsn 4226 . . . . . . . . . . 11 (𝑗 ∈ {{𝑍}} ↔ 𝑗 = {𝑍})
28 velsn 4226 . . . . . . . . . . 11 (𝑗 ∈ {𝑋} ↔ 𝑗 = 𝑋)
2927, 28orbi12i 542 . . . . . . . . . 10 ((𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
3026, 29bitri 264 . . . . . . . . 9 (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
3125, 30anbi12i 733 . . . . . . . 8 ((𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))
3220, 31syl6bb 276 . . . . . . 7 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
3317, 32sylbi 207 . . . . . 6 ((Idl‘𝑅) = {{𝑍}, 𝑋} → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
34333ad2ant3 1104 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
35 eqimss 3690 . . . . . . . . . . 11 (𝑖 = {𝑍} → 𝑖 ⊆ {𝑍})
3635orcd 406 . . . . . . . . . 10 (𝑖 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
3736adantr 480 . . . . . . . . 9 ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
3837a1d 25 . . . . . . . 8 ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
3938a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
40 eqimss 3690 . . . . . . . . . . 11 (𝑗 = {𝑍} → 𝑗 ⊆ {𝑍})
4140olcd 407 . . . . . . . . . 10 (𝑗 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4241adantl 481 . . . . . . . . 9 ((𝑖 = 𝑋𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4342a1d 25 . . . . . . . 8 ((𝑖 = 𝑋𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
4443a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = 𝑋𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
4536adantr 480 . . . . . . . . 9 ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4645a1d 25 . . . . . . . 8 ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
4746a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
482rneqi 5384 . . . . . . . . . . . . . 14 ran 𝐺 = ran (1st𝑅)
497, 48eqtri 2673 . . . . . . . . . . . . 13 𝑋 = ran (1st𝑅)
5049, 6, 8rngo1cl 33868 . . . . . . . . . . . 12 (𝑅 ∈ RingOps → 𝑈𝑋)
5150adantr 480 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → 𝑈𝑋)
526, 49, 8rngolidm 33866 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ 𝑈𝑋) → (𝑈𝐻𝑈) = 𝑈)
5350, 52mpdan 703 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑈𝐻𝑈) = 𝑈)
5453eleq1d 2715 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ∈ {𝑍}))
55 fvex 6239 . . . . . . . . . . . . . . . 16 (GId‘𝐻) ∈ V
568, 55eqeltri 2726 . . . . . . . . . . . . . . 15 𝑈 ∈ V
5756elsn 4225 . . . . . . . . . . . . . 14 (𝑈 ∈ {𝑍} ↔ 𝑈 = 𝑍)
5854, 57syl6bb 276 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 = 𝑍))
5958necon3bbid 2860 . . . . . . . . . . . 12 (𝑅 ∈ RingOps → (¬ (𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈𝑍))
6059biimpar 501 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ¬ (𝑈𝐻𝑈) ∈ {𝑍})
61 oveq1 6697 . . . . . . . . . . . . . 14 (𝑥 = 𝑈 → (𝑥𝐻𝑦) = (𝑈𝐻𝑦))
6261eleq1d 2715 . . . . . . . . . . . . 13 (𝑥 = 𝑈 → ((𝑥𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑦) ∈ {𝑍}))
6362notbid 307 . . . . . . . . . . . 12 (𝑥 = 𝑈 → (¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑦) ∈ {𝑍}))
64 oveq2 6698 . . . . . . . . . . . . . 14 (𝑦 = 𝑈 → (𝑈𝐻𝑦) = (𝑈𝐻𝑈))
6564eleq1d 2715 . . . . . . . . . . . . 13 (𝑦 = 𝑈 → ((𝑈𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑈) ∈ {𝑍}))
6665notbid 307 . . . . . . . . . . . 12 (𝑦 = 𝑈 → (¬ (𝑈𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑈) ∈ {𝑍}))
6763, 66rspc2ev 3355 . . . . . . . . . . 11 ((𝑈𝑋𝑈𝑋 ∧ ¬ (𝑈𝐻𝑈) ∈ {𝑍}) → ∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
6851, 51, 60, 67syl3anc 1366 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
69 rexnal2 3072 . . . . . . . . . 10 (∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
7068, 69sylib 208 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ¬ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
7170pm2.21d 118 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
72 raleq 3168 . . . . . . . . . 10 (𝑖 = 𝑋 → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍}))
73 raleq 3168 . . . . . . . . . . 11 (𝑗 = 𝑋 → (∀𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7473ralbidv 3015 . . . . . . . . . 10 (𝑗 = 𝑋 → (∀𝑥𝑋𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7572, 74sylan9bb 736 . . . . . . . . 9 ((𝑖 = 𝑋𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7675imbi1d 330 . . . . . . . 8 ((𝑖 = 𝑋𝑗 = 𝑋) → ((∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) ↔ (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
7771, 76syl5ibrcom 237 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = 𝑋𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
7839, 44, 47, 77ccased 1007 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
79783adant3 1101 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
8034, 79sylbid 230 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
8180ralrimivv 2999 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
822, 6, 7ispridl 33963 . . . 4 (𝑅 ∈ RingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
83823ad2ant1 1102 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
845, 15, 81, 83mpbir3and 1264 . 2 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (PrIdl‘𝑅))
852, 3isprrngo 33979 . 2 (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
861, 84, 85sylanbrc 699 1 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∪ cun 3605   ⊆ wss 3607  {csn 4210  {cpr 4212  ran crn 5144  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  GIdcgi 27472  RingOpscrngo 33823  Idlcidl 33936  PrIdlcpridl 33937  PrRingcprrng 33975 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-1st 7210  df-2nd 7211  df-grpo 27475  df-gid 27476  df-ginv 27477  df-ablo 27527  df-ass 33772  df-exid 33774  df-mgmOLD 33778  df-sgrOLD 33790  df-mndo 33796  df-rngo 33824  df-idl 33939  df-pridl 33940  df-prrngo 33977 This theorem is referenced by:  divrngpr  33982
 Copyright terms: Public domain W3C validator