This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lpir

Description: Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Assertion df-lpir LPIR = { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpir ⊢ LPIR
1 vw ⊢ 𝑤
2 crg ⊢ Ring
3 clidl ⊢ LIdeal
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( LIdeal ‘ 𝑤 )
6 clpidl ⊢ LPIdeal
7 4 6 cfv ⊢ ( LPIdeal ‘ 𝑤 )
8 5 7 wceq ⊢ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 )
9 8 1 2 crab ⊢ { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }
10 0 9 wceq ⊢ LPIR = { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }