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	|- A = ( ( subringAlg ` R ) ` V )
	sraidom.2	|- B = ( Base ` R )
	sraidom.3	|- ( ph -> R e. IDomn )
	sraidom.4	|- ( ph -> V C_ B )
Assertion	sraidom	|- ( ph -> A e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		sraidom.1	|- A = ( ( subringAlg ` R ) ` V )
2		sraidom.2	|- B = ( Base ` R )
3		sraidom.3	|- ( ph -> R e. IDomn )
4		sraidom.4	|- ( ph -> V C_ B )
5		eqidd	|- ( ph -> ( Base ` R ) = ( Base ` R ) )
6	1	a1i	|- ( ph -> A = ( ( subringAlg ` R ) ` V ) )
7	4 2	sseqtrdi	|- ( ph -> V C_ ( Base ` R ) )
8	6 7	srabase	|- ( ph -> ( Base ` R ) = ( Base ` A ) )
9	6 7	sraaddg	|- ( ph -> ( +g ` R ) = ( +g ` A ) )
10	9	oveqdr	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` A ) y ) )
11	6 7	sramulr	|- ( ph -> ( .r ` R ) = ( .r ` A ) )
12	11	oveqdr	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` A ) y ) )
13	5 8 10 12	idompropd	|- ( ph -> ( R e. IDomn <-> A e. IDomn ) )
14	3 13	mpbid	|- ( ph -> A e. IDomn )