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=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
	sraidom.2	$$⊢B={\mathrm{Base}}_R$$
	sraidom.3	$$⊢\phi \to R\in \mathrm{IDomn}$$
	sraidom.4	$$⊢\phi \to V\subseteq B$$
Assertion	sraidom	$$⊢\phi \to A\in \mathrm{IDomn}$$

Proof

Step	Hyp	Ref	Expression
1		sraidom.1	$$⊢A=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
2		sraidom.2	$$⊢B={\mathrm{Base}}_R$$
3		sraidom.3	$$⊢\phi \to R\in \mathrm{IDomn}$$
4		sraidom.4	$$⊢\phi \to V\subseteq B$$
5		eqidd	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	1	a1i	$$⊢\phi \to A=\mathrm{subringAlg}\left(R\right)\left(V\right)$$
7	4 2	sseqtrdi	$$⊢\phi \to V\subseteq {\mathrm{Base}}_R$$
8	6 7	srabase	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_A$$
9	6 7	sraaddg	$$⊢\phi \to {+}_R={+}_A$$
10	9	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{R}y=x{+}_{A}y$$
11	6 7	sramulr	$$⊢\phi \to {\cdot }_R={\cdot }_A$$
12	11	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{\cdot }_{R}y=x{\cdot }_{A}y$$
13	5 8 10 12	idompropd	$$⊢\phi \to \left(R\in \mathrm{IDomn}\leftrightarrow A\in \mathrm{IDomn}\right)$$
14	3 13	mpbid	$$⊢\phi \to A\in \mathrm{IDomn}$$