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 ) )