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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
domnpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
domnpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
domnpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion idompropd ( 𝜑 → ( 𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn ) )

Proof

Step Hyp Ref Expression
1 domnpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 domnpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 domnpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 domnpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5 1 2 3 4 crngpropd ⊢ ( 𝜑 → ( 𝐾 ∈ CRing ↔ 𝐿 ∈ CRing ) )
6 1 2 3 4 domnpropd ⊢ ( 𝜑 → ( 𝐾 ∈ Domn ↔ 𝐿 ∈ Domn ) )
7 5 6 anbi12d ⊢ ( 𝜑 → ( ( 𝐾 ∈ CRing ∧ 𝐾 ∈ Domn ) ↔ ( 𝐿 ∈ CRing ∧ 𝐿 ∈ Domn ) ) )
8 isidom ⊢ ( 𝐾 ∈ IDomn ↔ ( 𝐾 ∈ CRing ∧ 𝐾 ∈ Domn ) )
9 isidom ⊢ ( 𝐿 ∈ IDomn ↔ ( 𝐿 ∈ CRing ∧ 𝐿 ∈ Domn ) )
10 7 8 9 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn ) )