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 ⊢ φ → B = Base K
domnpropd.2 ⊢ φ → B = Base L
domnpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
domnpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion idompropd ⊢ φ → K ∈ IDomn ↔ L ∈ IDomn

Proof

Step Hyp Ref Expression
1 domnpropd.1 ⊢ φ → B = Base K
2 domnpropd.2 ⊢ φ → B = Base L
3 domnpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 domnpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
5 1 2 3 4 crngpropd ⊢ φ → K ∈ CRing ↔ L ∈ CRing
6 1 2 3 4 domnpropd ⊢ φ → K ∈ Domn ↔ L ∈ Domn
7 5 6 anbi12d ⊢ φ → K ∈ CRing ∧ K ∈ Domn ↔ L ∈ CRing ∧ L ∈ Domn
8 isidom ⊢ K ∈ IDomn ↔ K ∈ CRing ∧ K ∈ Domn
9 isidom ⊢ L ∈ IDomn ↔ L ∈ CRing ∧ L ∈ Domn
10 7 8 9 3bitr4g ⊢ φ → K ∈ IDomn ↔ L ∈ IDomn