Metamath Proof Explorer

Theorem lpival

Description: Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p ⊢ P = LPIdeal ⁡ R
lpival.k ⊢ K = RSpan ⁡ R
lpival.b ⊢ B = Base R
Assertion lpival ⊢ R ∈ Ring → P = ⋃ g ∈ B K ⁡ g

Proof

Step Hyp Ref Expression
1 lpival.p ⊢ P = LPIdeal ⁡ R
2 lpival.k ⊢ K = RSpan ⁡ R
3 lpival.b ⊢ B = Base R
4 fveq2 ⊢ r = R → Base r = Base R
5 fveq2 ⊢ r = R → RSpan ⁡ r = RSpan ⁡ R
6 5 fveq1d ⊢ r = R → RSpan ⁡ r ⁡ g = RSpan ⁡ R ⁡ g
7 6 sneqd ⊢ r = R → RSpan ⁡ r ⁡ g = RSpan ⁡ R ⁡ g
8 4 7 iuneq12d ⊢ r = R → ⋃ g ∈ Base r RSpan ⁡ r ⁡ g = ⋃ g ∈ Base R RSpan ⁡ R ⁡ g
9 df-lpidl ⊢ LPIdeal = r ∈ Ring ⟼ ⋃ g ∈ Base r RSpan ⁡ r ⁡ g
10 fvex ⊢ RSpan ⁡ R ∈ V
11 10 rnex ⊢ ran ⁡ RSpan ⁡ R ∈ V
12 snex ⊢ ∅ ∈ V
13 11 12 unex ⊢ ran ⁡ RSpan ⁡ R ∪ ∅ ∈ V
14 iunss ⊢ ⋃ g ∈ Base R RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅ ↔ ∀ g ∈ Base R RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅
15 fvrn0 ⊢ RSpan ⁡ R ⁡ g ∈ ran ⁡ RSpan ⁡ R ∪ ∅
16 snssi ⊢ RSpan ⁡ R ⁡ g ∈ ran ⁡ RSpan ⁡ R ∪ ∅ → RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅
17 15 16 ax-mp ⊢ RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅
18 17 a1i ⊢ g ∈ Base R → RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅
19 14 18 mprgbir ⊢ ⋃ g ∈ Base R RSpan ⁡ R ⁡ g ⊆ ran ⁡ RSpan ⁡ R ∪ ∅
20 13 19 ssexi ⊢ ⋃ g ∈ Base R RSpan ⁡ R ⁡ g ∈ V
21 8 9 20 fvmpt ⊢ R ∈ Ring → LPIdeal ⁡ R = ⋃ g ∈ Base R RSpan ⁡ R ⁡ g
22 iuneq1 ⊢ B = Base R → ⋃ g ∈ B K ⁡ g = ⋃ g ∈ Base R K ⁡ g
23 3 22 ax-mp ⊢ ⋃ g ∈ B K ⁡ g = ⋃ g ∈ Base R K ⁡ g
24 2 fveq1i ⊢ K ⁡ g = RSpan ⁡ R ⁡ g
25 24 sneqi ⊢ K ⁡ g = RSpan ⁡ R ⁡ g
26 25 a1i ⊢ g ∈ Base R → K ⁡ g = RSpan ⁡ R ⁡ g
27 26 iuneq2i ⊢ ⋃ g ∈ Base R K ⁡ g = ⋃ g ∈ Base R RSpan ⁡ R ⁡ g
28 23 27 eqtri ⊢ ⋃ g ∈ B K ⁡ g = ⋃ g ∈ Base R RSpan ⁡ R ⁡ g
29 21 1 28 3eqtr4g ⊢ R ∈ Ring → P = ⋃ g ∈ B K ⁡ g