Metamath Proof Explorer

Definition df-pid

Description: Aprincipal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015)

		Ref	Expression
	Assertion	df-pid	\|- PID = ( IDomn i^i LPIR )

Detailed syntax breakdown


 |-  PID
 |-  IDomn
 |-  LPIR
 |-  ( IDomn i^i LPIR )
 |-  PID = ( IDomn i^i LPIR )

Step	Hyp	Ref	Expression
0		cpid	\|- PID
1		cidom	\|- IDomn
2		clpir	\|- LPIR
3	1 2	cin	\|- ( IDomn i^i LPIR )
4	0 3	wceq	\|- PID = ( IDomn i^i LPIR )