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

Metamath Proof Explorer

Theorem idompropd

Description: If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd . (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses domnpropd.1 
|- ( ph -> B = ( Base ` K ) )
domnpropd.2 
|- ( ph -> B = ( Base ` L ) )
domnpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
domnpropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion idompropd 
|- ( ph -> ( K e. IDomn <-> L e. IDomn ) )

Proof

Step Hyp Ref Expression
1 domnpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 domnpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 domnpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 domnpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 crngpropd 
 |-  ( ph -> ( K e. CRing <-> L e. CRing ) )
6 1 2 3 4 domnpropd 
 |-  ( ph -> ( K e. Domn <-> L e. Domn ) )
7 5 6 anbi12d 
 |-  ( ph -> ( ( K e. CRing /\ K e. Domn ) <-> ( L e. CRing /\ L e. Domn ) ) )
8 isidom 
 |-  ( K e. IDomn <-> ( K e. CRing /\ K e. Domn ) )
9 isidom 
 |-  ( L e. IDomn <-> ( L e. CRing /\ L e. Domn ) )
10 7 8 9 3bitr4g 
 |-  ( ph -> ( K e. IDomn <-> L e. IDomn ) )