Theorem lpi1

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

	Ref	Expression
Hypotheses	lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpi1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	lpi1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2		lpi1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	2 3	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
5		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
6	5 2 3	rsp1	⊢ ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) = 𝐵 )
7	6	eqcomd	⊢ ( 𝑅 ∈ Ring → 𝐵 = ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) )
8		sneq	⊢ ( 𝑔 = ( 1r ‘ 𝑅 ) → { 𝑔 } = { ( 1r ‘ 𝑅 ) } )
9	8	fveq2d	⊢ ( 𝑔 = ( 1r ‘ 𝑅 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) )
10	9	rspceeqv	⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ 𝐵 = ( ( RSpan ‘ 𝑅 ) ‘ { ( 1r ‘ 𝑅 ) } ) ) → ∃ 𝑔 ∈ 𝐵 𝐵 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) )
11	4 7 10	syl2anc	⊢ ( 𝑅 ∈ Ring → ∃ 𝑔 ∈ 𝐵 𝐵 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) )
12	1 5 2	islpidl	⊢ ( 𝑅 ∈ Ring → ( 𝐵 ∈ 𝑃 ↔ ∃ 𝑔 ∈ 𝐵 𝐵 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ) )
13	11 12	mpbird	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑃 )