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	$⊢ φ \to B = {Base}_{K}$
		domnpropd.2	$⊢ φ \to B = {Base}_{L}$
		domnpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
		domnpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	Assertion	idompropd	$⊢ φ \to (K \in IDomn \leftrightarrow L \in IDomn)$

Proof

Step	Hyp	Ref	Expression
1		domnpropd.1	$⊢ φ \to B = {Base}_{K}$
2		domnpropd.2	$⊢ φ \to B = {Base}_{L}$
3		domnpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		domnpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5	1 2 3 4	crngpropd	$⊢ φ \to (K \in CRing \leftrightarrow L \in CRing)$
6	1 2 3 4	domnpropd	$⊢ φ \to (K \in Domn \leftrightarrow L \in Domn)$
7	5 6	anbi12d	$⊢ φ \to ((K \in CRing \land K \in Domn) \leftrightarrow (L \in CRing \land L \in Domn))$
8		isidom	$⊢ K \in IDomn \leftrightarrow (K \in CRing \land K \in Domn)$
9		isidom	$⊢ L \in IDomn \leftrightarrow (L \in CRing \land L \in Domn)$
10	7 8 9	3bitr4g	$⊢ φ \to (K \in IDomn \leftrightarrow L \in IDomn)$