Metamath Proof Explorer

Theorem lpi1

Description: The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p ⊢ P = LPIdeal ⁡ R
lpi1.b ⊢ B = Base R
Assertion lpi1 ⊢ R ∈ Ring → B ∈ P

Proof

Step Hyp Ref Expression
1 lpival.p ⊢ P = LPIdeal ⁡ R
2 lpi1.b ⊢ B = Base R
3 eqid ⊢ 1 R = 1 R
4 2 3 ringidcl ⊢ R ∈ Ring → 1 R ∈ B
5 eqid ⊢ RSpan ⁡ R = RSpan ⁡ R
6 5 2 3 rsp1 ⊢ R ∈ Ring → RSpan ⁡ R ⁡ 1 R = B
7 6 eqcomd ⊢ R ∈ Ring → B = RSpan ⁡ R ⁡ 1 R
8 sneq ⊢ g = 1 R → g = 1 R
9 8 fveq2d ⊢ g = 1 R → RSpan ⁡ R ⁡ g = RSpan ⁡ R ⁡ 1 R
10 9 rspceeqv ⊢ 1 R ∈ B ∧ B = RSpan ⁡ R ⁡ 1 R → ∃ g ∈ B B = RSpan ⁡ R ⁡ g
11 4 7 10 syl2anc ⊢ R ∈ Ring → ∃ g ∈ B B = RSpan ⁡ R ⁡ g
12 1 5 2 islpidl ⊢ R ∈ Ring → B ∈ P ↔ ∃ g ∈ B B = RSpan ⁡ R ⁡ g
13 11 12 mpbird ⊢ R ∈ Ring → B ∈ P