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