Metamath Proof Explorer

Theorem ezidom

Description: The Eisenstein integers form an integral domain. (Contributed by AV, 26-Oct-2026)

Ref Expression
Assertion ezidom 
|- ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) e. IDomn

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) = ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) )
2 ezsubrg 
 |-  ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld )
3 1 2 subrgccidom 
 |-  ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) e. IDomn