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

Metamath Proof Explorer

Theorem sradrng

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

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

Proof

Step Hyp Ref Expression
1 sradrng.1 
 |-  A = ( ( subringAlg ` R ) ` V )
2 sradrng.2 
 |-  B = ( Base ` R )
3 drngring 
 |-  ( R e. DivRing -> R e. Ring )
4 1 2 sraring 
 |-  ( ( R e. Ring /\ V C_ B ) -> A e. Ring )
5 3 4 sylan 
 |-  ( ( R e. DivRing /\ V C_ B ) -> A e. Ring )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 6 7 8 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) )
10 9 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) )
11 10 adantr 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) )
12 eqidd 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( Base ` R ) = ( Base ` R ) )
13 1 a1i 
 |-  ( ( R e. DivRing /\ V C_ B ) -> A = ( ( subringAlg ` R ) ` V ) )
14 simpr 
 |-  ( ( R e. DivRing /\ V C_ B ) -> V C_ B )
15 14 2 sseqtrdi 
 |-  ( ( R e. DivRing /\ V C_ B ) -> V C_ ( Base ` R ) )
16 13 15 srabase 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( Base ` R ) = ( Base ` A ) )
17 13 15 sramulr 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( .r ` R ) = ( .r ` A ) )
18 17 oveqdr 
 |-  ( ( ( R e. DivRing /\ V C_ B ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` A ) y ) )
19 12 16 18 unitpropd 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( Unit ` R ) = ( Unit ` A ) )
20 eqidd 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( 0g ` R ) = ( 0g ` R ) )
21 13 20 15 sralmod0 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( 0g ` R ) = ( 0g ` A ) )
22 21 sneqd 
 |-  ( ( R e. DivRing /\ V C_ B ) -> { ( 0g ` R ) } = { ( 0g ` A ) } )
23 16 22 difeq12d 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( ( Base ` A ) \ { ( 0g ` A ) } ) )
24 11 19 23 3eqtr3d 
 |-  ( ( R e. DivRing /\ V C_ B ) -> ( Unit ` A ) = ( ( Base ` A ) \ { ( 0g ` A ) } ) )
25 eqid 
 |-  ( Base ` A ) = ( Base ` A )
26 eqid 
 |-  ( Unit ` A ) = ( Unit ` A )
27 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
28 25 26 27 isdrng 
 |-  ( A e. DivRing <-> ( A e. Ring /\ ( Unit ` A ) = ( ( Base ` A ) \ { ( 0g ` A ) } ) ) )
29 5 24 28 sylanbrc 
 |-  ( ( R e. DivRing /\ V C_ B ) -> A e. DivRing )