| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . 4
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) | 
| 2 |  | fveq2 6906 | . . . . . 6
⊢ (𝑟 = 𝑅 → (RSpan‘𝑟) = (RSpan‘𝑅)) | 
| 3 | 2 | fveq1d 6908 | . . . . 5
⊢ (𝑟 = 𝑅 → ((RSpan‘𝑟)‘{𝑔}) = ((RSpan‘𝑅)‘{𝑔})) | 
| 4 | 3 | sneqd 4638 | . . . 4
⊢ (𝑟 = 𝑅 → {((RSpan‘𝑟)‘{𝑔})} = {((RSpan‘𝑅)‘{𝑔})}) | 
| 5 | 1, 4 | iuneq12d 5021 | . . 3
⊢ (𝑟 = 𝑅 → ∪
𝑔 ∈ (Base‘𝑟){((RSpan‘𝑟)‘{𝑔})} = ∪
𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})}) | 
| 6 |  | df-lpidl 21332 | . . 3
⊢ LPIdeal =
(𝑟 ∈ Ring ↦
∪ 𝑔 ∈ (Base‘𝑟){((RSpan‘𝑟)‘{𝑔})}) | 
| 7 |  | fvex 6919 | . . . . . 6
⊢
(RSpan‘𝑅)
∈ V | 
| 8 | 7 | rnex 7932 | . . . . 5
⊢ ran
(RSpan‘𝑅) ∈
V | 
| 9 |  | p0ex 5384 | . . . . 5
⊢ {∅}
∈ V | 
| 10 | 8, 9 | unex 7764 | . . . 4
⊢ (ran
(RSpan‘𝑅) ∪
{∅}) ∈ V | 
| 11 |  | iunss 5045 | . . . . 5
⊢ (∪ 𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪ {∅}) ↔
∀𝑔 ∈
(Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪
{∅})) | 
| 12 |  | fvrn0 6936 | . . . . . . 7
⊢
((RSpan‘𝑅)‘{𝑔}) ∈ (ran (RSpan‘𝑅) ∪ {∅}) | 
| 13 |  | snssi 4808 | . . . . . . 7
⊢
(((RSpan‘𝑅)‘{𝑔}) ∈ (ran (RSpan‘𝑅) ∪ {∅}) →
{((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪
{∅})) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . 6
⊢
{((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪
{∅}) | 
| 15 | 14 | a1i 11 | . . . . 5
⊢ (𝑔 ∈ (Base‘𝑅) → {((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪
{∅})) | 
| 16 | 11, 15 | mprgbir 3068 | . . . 4
⊢ ∪ 𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} ⊆ (ran (RSpan‘𝑅) ∪
{∅}) | 
| 17 | 10, 16 | ssexi 5322 | . . 3
⊢ ∪ 𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} ∈ V | 
| 18 | 5, 6, 17 | fvmpt 7016 | . 2
⊢ (𝑅 ∈ Ring →
(LPIdeal‘𝑅) =
∪ 𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})}) | 
| 19 |  | lpival.p | . 2
⊢ 𝑃 = (LPIdeal‘𝑅) | 
| 20 |  | lpival.b | . . . 4
⊢ 𝐵 = (Base‘𝑅) | 
| 21 |  | iuneq1 5008 | . . . 4
⊢ (𝐵 = (Base‘𝑅) → ∪
𝑔 ∈ 𝐵 {(𝐾‘{𝑔})} = ∪
𝑔 ∈ (Base‘𝑅){(𝐾‘{𝑔})}) | 
| 22 | 20, 21 | ax-mp 5 | . . 3
⊢ ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})} = ∪
𝑔 ∈ (Base‘𝑅){(𝐾‘{𝑔})} | 
| 23 |  | lpival.k | . . . . . . 7
⊢ 𝐾 = (RSpan‘𝑅) | 
| 24 | 23 | fveq1i 6907 | . . . . . 6
⊢ (𝐾‘{𝑔}) = ((RSpan‘𝑅)‘{𝑔}) | 
| 25 | 24 | sneqi 4637 | . . . . 5
⊢ {(𝐾‘{𝑔})} = {((RSpan‘𝑅)‘{𝑔})} | 
| 26 | 25 | a1i 11 | . . . 4
⊢ (𝑔 ∈ (Base‘𝑅) → {(𝐾‘{𝑔})} = {((RSpan‘𝑅)‘{𝑔})}) | 
| 27 | 26 | iuneq2i 5013 | . . 3
⊢ ∪ 𝑔 ∈ (Base‘𝑅){(𝐾‘{𝑔})} = ∪
𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} | 
| 28 | 22, 27 | eqtri 2765 | . 2
⊢ ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})} = ∪
𝑔 ∈ (Base‘𝑅){((RSpan‘𝑅)‘{𝑔})} | 
| 29 | 18, 19, 28 | 3eqtr4g 2802 | 1
⊢ (𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 {(𝐾‘{𝑔})}) |