sraidom

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

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

Metamath Proof Explorer