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