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

Theorem pzriprnglem8 21375
Description: Lemma 8 for pzriprng 21384: 𝐼 resp. 𝐽 is a two-sided ideal of the non-unital ring 𝑅. (Contributed by AV, 21-Mar-2025.)
Hypotheses
Ref Expression
pzriprng.r 𝑅 = (β„€ring Γ—s β„€ring)
pzriprng.i 𝐼 = (β„€ Γ— {0})
pzriprng.j 𝐽 = (𝑅 β†Ύs 𝐼)
Assertion
Ref Expression
pzriprnglem8 𝐼 ∈ (2Idealβ€˜π‘…)

Proof of Theorem pzriprnglem8
Dummy variables π‘₯ 𝑦 π‘Ž 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pzriprng.r . . . . . . 7 𝑅 = (β„€ring Γ—s β„€ring)
21pzriprnglem2 21369 . . . . . 6 (Baseβ€˜π‘…) = (β„€ Γ— β„€)
32eleq2i 2819 . . . . 5 (π‘₯ ∈ (Baseβ€˜π‘…) ↔ π‘₯ ∈ (β„€ Γ— β„€))
4 elxp2 5693 . . . . 5 (π‘₯ ∈ (β„€ Γ— β„€) ↔ βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)
53, 4bitri 275 . . . 4 (π‘₯ ∈ (Baseβ€˜π‘…) ↔ βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)
6 pzriprng.i . . . . 5 𝐼 = (β„€ Γ— {0})
71, 6pzriprnglem3 21370 . . . 4 (𝑦 ∈ 𝐼 ↔ βˆƒπ‘ ∈ β„€ 𝑦 = βŸ¨π‘, 0⟩)
8 simpll 764 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ π‘Ž ∈ β„€)
9 simpr 484 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ 𝑐 ∈ β„€)
108, 9zmulcld 12676 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (π‘Ž Β· 𝑐) ∈ β„€)
11 zcn 12567 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ β„€ β†’ 𝑏 ∈ β„‚)
1211adantl 481 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) β†’ 𝑏 ∈ β„‚)
1312adantr 480 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ 𝑏 ∈ β„‚)
1413mul01d 11417 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑏 Β· 0) = 0)
15 ovex 7438 . . . . . . . . . . . . . . 15 (𝑏 Β· 0) ∈ V
1615elsn 4638 . . . . . . . . . . . . . 14 ((𝑏 Β· 0) ∈ {0} ↔ (𝑏 Β· 0) = 0)
1714, 16sylibr 233 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑏 Β· 0) ∈ {0})
1810, 17opelxpd 5708 . . . . . . . . . . . 12 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ ⟨(π‘Ž Β· 𝑐), (𝑏 Β· 0)⟩ ∈ (β„€ Γ— {0}))
199, 8zmulcld 12676 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑐 Β· π‘Ž) ∈ β„€)
2013mul02d 11416 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (0 Β· 𝑏) = 0)
21 ovex 7438 . . . . . . . . . . . . . . 15 (0 Β· 𝑏) ∈ V
2221elsn 4638 . . . . . . . . . . . . . 14 ((0 Β· 𝑏) ∈ {0} ↔ (0 Β· 𝑏) = 0)
2320, 22sylibr 233 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (0 Β· 𝑏) ∈ {0})
2419, 23opelxpd 5708 . . . . . . . . . . . 12 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ ⟨(𝑐 Β· π‘Ž), (0 Β· 𝑏)⟩ ∈ (β„€ Γ— {0}))
25 zringbas 21340 . . . . . . . . . . . . . . 15 β„€ = (Baseβ€˜β„€ring)
26 zringring 21336 . . . . . . . . . . . . . . . 16 β„€ring ∈ Ring
2726a1i 11 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ β„€ring ∈ Ring)
28 simplr 766 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ 𝑏 ∈ β„€)
29 0zd 12574 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ 0 ∈ β„€)
3028, 29zmulcld 12676 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑏 Β· 0) ∈ β„€)
31 zringmulr 21344 . . . . . . . . . . . . . . 15 Β· = (.rβ€˜β„€ring)
32 eqid 2726 . . . . . . . . . . . . . . 15 (.rβ€˜π‘…) = (.rβ€˜π‘…)
331, 25, 25, 27, 27, 8, 28, 9, 29, 10, 30, 31, 31, 32xpsmul 17530 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) = ⟨(π‘Ž Β· 𝑐), (𝑏 Β· 0)⟩)
3433eleq1d 2812 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ ((βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0}) ↔ ⟨(π‘Ž Β· 𝑐), (𝑏 Β· 0)⟩ ∈ (β„€ Γ— {0})))
35 simpl 482 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ 𝑐 ∈ β„€)
36 simprl 768 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ π‘Ž ∈ β„€)
3735, 36zmulcld 12676 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ (𝑐 Β· π‘Ž) ∈ β„€)
3837ancoms 458 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑐 Β· π‘Ž) ∈ β„€)
39 0zd 12574 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ 0 ∈ β„€)
40 simprr 770 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ 𝑏 ∈ β„€)
4139, 40zmulcld 12676 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ β„€ ∧ (π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€)) β†’ (0 Β· 𝑏) ∈ β„€)
4241ancoms 458 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (0 Β· 𝑏) ∈ β„€)
431, 25, 25, 27, 27, 9, 29, 8, 28, 38, 42, 31, 31, 32xpsmul 17530 . . . . . . . . . . . . . 14 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) = ⟨(𝑐 Β· π‘Ž), (0 Β· 𝑏)⟩)
4443eleq1d 2812 . . . . . . . . . . . . 13 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ ((βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0}) ↔ ⟨(𝑐 Β· π‘Ž), (0 Β· 𝑏)⟩ ∈ (β„€ Γ— {0})))
4534, 44anbi12d 630 . . . . . . . . . . . 12 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (((βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0}) ∧ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0})) ↔ (⟨(π‘Ž Β· 𝑐), (𝑏 Β· 0)⟩ ∈ (β„€ Γ— {0}) ∧ ⟨(𝑐 Β· π‘Ž), (0 Β· 𝑏)⟩ ∈ (β„€ Γ— {0}))))
4618, 24, 45mpbir2and 710 . . . . . . . . . . 11 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ ((βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0}) ∧ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0})))
4746adantr 480 . . . . . . . . . 10 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ ((βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0}) ∧ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0})))
48 oveq12 7414 . . . . . . . . . . . . . 14 ((π‘₯ = βŸ¨π‘Ž, π‘βŸ© ∧ 𝑦 = βŸ¨π‘, 0⟩) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩))
4948ancoms 458 . . . . . . . . . . . . 13 ((𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩))
5049adantl 481 . . . . . . . . . . . 12 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩))
516a1i 11 . . . . . . . . . . . 12 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ 𝐼 = (β„€ Γ— {0}))
5250, 51eleq12d 2821 . . . . . . . . . . 11 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ↔ (βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0})))
53 oveq12 7414 . . . . . . . . . . . . 13 ((𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©) β†’ (𝑦(.rβ€˜π‘…)π‘₯) = (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©))
5453adantl 481 . . . . . . . . . . . 12 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ (𝑦(.rβ€˜π‘…)π‘₯) = (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©))
5554, 51eleq12d 2821 . . . . . . . . . . 11 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ ((𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼 ↔ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0})))
5652, 55anbi12d 630 . . . . . . . . . 10 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ (((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼) ↔ ((βŸ¨π‘Ž, π‘βŸ©(.rβ€˜π‘…)βŸ¨π‘, 0⟩) ∈ (β„€ Γ— {0}) ∧ (βŸ¨π‘, 0⟩(.rβ€˜π‘…)βŸ¨π‘Ž, π‘βŸ©) ∈ (β„€ Γ— {0}))))
5747, 56mpbird 257 . . . . . . . . 9 ((((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) ∧ (𝑦 = βŸ¨π‘, 0⟩ ∧ π‘₯ = βŸ¨π‘Ž, π‘βŸ©)) β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))
5857exp32 420 . . . . . . . 8 (((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) ∧ 𝑐 ∈ β„€) β†’ (𝑦 = βŸ¨π‘, 0⟩ β†’ (π‘₯ = βŸ¨π‘Ž, π‘βŸ© β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))))
5958rexlimdva 3149 . . . . . . 7 ((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) β†’ (βˆƒπ‘ ∈ β„€ 𝑦 = βŸ¨π‘, 0⟩ β†’ (π‘₯ = βŸ¨π‘Ž, π‘βŸ© β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))))
6059com23 86 . . . . . 6 ((π‘Ž ∈ β„€ ∧ 𝑏 ∈ β„€) β†’ (π‘₯ = βŸ¨π‘Ž, π‘βŸ© β†’ (βˆƒπ‘ ∈ β„€ 𝑦 = βŸ¨π‘, 0⟩ β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))))
6160rexlimivv 3193 . . . . 5 (βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ π‘₯ = βŸ¨π‘Ž, π‘βŸ© β†’ (βˆƒπ‘ ∈ β„€ 𝑦 = βŸ¨π‘, 0⟩ β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼)))
6261imp 406 . . . 4 ((βˆƒπ‘Ž ∈ β„€ βˆƒπ‘ ∈ β„€ π‘₯ = βŸ¨π‘Ž, π‘βŸ© ∧ βˆƒπ‘ ∈ β„€ 𝑦 = βŸ¨π‘, 0⟩) β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))
635, 7, 62syl2anb 597 . . 3 ((π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐼) β†’ ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))
6463rgen2 3191 . 2 βˆ€π‘₯ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ 𝐼 ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼)
651pzriprnglem1 21368 . . 3 𝑅 ∈ Rng
661, 6pzriprnglem4 21371 . . 3 𝐼 ∈ (SubGrpβ€˜π‘…)
67 eqid 2726 . . . 4 (2Idealβ€˜π‘…) = (2Idealβ€˜π‘…)
68 eqid 2726 . . . 4 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
6967, 68, 32df2idl2rng 21113 . . 3 ((𝑅 ∈ Rng ∧ 𝐼 ∈ (SubGrpβ€˜π‘…)) β†’ (𝐼 ∈ (2Idealβ€˜π‘…) ↔ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ 𝐼 ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼)))
7065, 66, 69mp2an 689 . 2 (𝐼 ∈ (2Idealβ€˜π‘…) ↔ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ 𝐼 ((π‘₯(.rβ€˜π‘…)𝑦) ∈ 𝐼 ∧ (𝑦(.rβ€˜π‘…)π‘₯) ∈ 𝐼))
7164, 70mpbir 230 1 𝐼 ∈ (2Idealβ€˜π‘…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  βˆƒwrex 3064  {csn 4623  βŸ¨cop 4629   Γ— cxp 5667  β€˜cfv 6537  (class class class)co 7405  β„‚cc 11110  0cc0 11112   Β· cmul 11117  β„€cz 12562  Basecbs 17153   β†Ύs cress 17182  .rcmulr 17207   Γ—s cxps 17461  SubGrpcsubg 19047  Rngcrng 20057  Ringcrg 20138  2Idealc2idl 21106  β„€ringczring 21333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-tpos 8212  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13491  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-0g 17396  df-prds 17402  df-imas 17463  df-xps 17465  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-grp 18866  df-minusg 18867  df-subg 19050  df-cmn 19702  df-abl 19703  df-mgp 20040  df-rng 20058  df-ur 20087  df-ring 20140  df-cring 20141  df-oppr 20236  df-subrng 20446  df-subrg 20471  df-lss 20779  df-sra 21021  df-rgmod 21022  df-lidl 21067  df-2idl 21107  df-cnfld 21241  df-zring 21334
This theorem is referenced by:  pzriprnglem12  21379  pzriprnglem13  21380  pzriprngALT  21382  pzriprng1ALT  21383
  Copyright terms: Public domain W3C validator