Theorem lpi0

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

	Ref	Expression
Hypotheses	lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpi0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lpi0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2		lpi0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
5		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
6	5 2	rsp0	⊢ ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ { 0 } ) = { 0 } )
7	6	eqcomd	⊢ ( 𝑅 ∈ Ring → { 0 } = ( ( RSpan ‘ 𝑅 ) ‘ { 0 } ) )
8		sneq	⊢ ( 𝑔 = 0 → { 𝑔 } = { 0 } )
9	8	fveq2d	⊢ ( 𝑔 = 0 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 0 } ) )
10	9	rspceeqv	⊢ ( ( 0 ∈ ( Base ‘ 𝑅 ) ∧ { 0 } = ( ( RSpan ‘ 𝑅 ) ‘ { 0 } ) ) → ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) { 0 } = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) )
11	4 7 10	syl2anc	⊢ ( 𝑅 ∈ Ring → ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) { 0 } = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) )
12	1 5 3	islpidl	⊢ ( 𝑅 ∈ Ring → ( { 0 } ∈ 𝑃 ↔ ∃ 𝑔 ∈ ( Base ‘ 𝑅 ) { 0 } = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ) )
13	11 12	mpbird	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑃 )