This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )