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

Metamath Proof Explorer

Theorem sraring

Description: Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023)

Ref Expression
Hypotheses sraring.1 
|- A = ( ( subringAlg ` R ) ` V )
sraring.2 
|- B = ( Base ` R )
Assertion sraring 
|- ( ( R e. Ring /\ V C_ B ) -> A e. Ring )

Proof

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