Theorem sraidom

Description: Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	sraidom.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
	sraidom.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
	sraidom.3	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	sraidom.4	⊢ ( 𝜑 → 𝑉 ⊆ 𝐵 )
Assertion	sraidom	⊢ ( 𝜑 → 𝐴 ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		sraidom.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
2		sraidom.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		sraidom.3	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
4		sraidom.4	⊢ ( 𝜑 → 𝑉 ⊆ 𝐵 )
5		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
6	1	a1i	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 ) )
7	4 2	sseqtrdi	⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝑅 ) )
8	6 7	srabase	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐴 ) )
9	6 7	sraaddg	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐴 ) )
10	9	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
11	6 7	sramulr	⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐴 ) )
12	11	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
13	5 8 10 12	idompropd	⊢ ( 𝜑 → ( 𝑅 ∈ IDomn ↔ 𝐴 ∈ IDomn ) )
14	3 13	mpbid	⊢ ( 𝜑 → 𝐴 ∈ IDomn )