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 
|- 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 )