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

Metamath Proof Explorer

Theorem fidomndrng

Description: A finite domain is a division ring. Note that Wedderburn's little theorem (not proved) states that finite division rings are fields. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis fidomndrng.b 
|- B = ( Base ` R )
Assertion fidomndrng 
|- ( B e. Fin -> ( R e. Domn <-> R e. DivRing ) )

Proof

Step Hyp Ref Expression
1 fidomndrng.b 
 |-  B = ( Base ` R )
2 domnring 
 |-  ( R e. Domn -> R e. Ring )
3 2 adantl 
 |-  ( ( B e. Fin /\ R e. Domn ) -> R e. Ring )
4 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
5 4 adantl 
 |-  ( ( B e. Fin /\ R e. Domn ) -> R e. NzRing )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 6 7 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
9 5 8 syl 
 |-  ( ( B e. Fin /\ R e. Domn ) -> ( 1r ` R ) =/= ( 0g ` R ) )
10 9 neneqd 
 |-  ( ( B e. Fin /\ R e. Domn ) -> -. ( 1r ` R ) = ( 0g ` R ) )
11 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
12 11 7 6 0unit 
 |-  ( R e. Ring -> ( ( 0g ` R ) e. ( Unit ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
13 3 12 syl 
 |-  ( ( B e. Fin /\ R e. Domn ) -> ( ( 0g ` R ) e. ( Unit ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
14 10 13 mtbird 
 |-  ( ( B e. Fin /\ R e. Domn ) -> -. ( 0g ` R ) e. ( Unit ` R ) )
15 disjsn 
 |-  ( ( ( Unit ` R ) i^i { ( 0g ` R ) } ) = (/) <-> -. ( 0g ` R ) e. ( Unit ` R ) )
16 14 15 sylibr 
 |-  ( ( B e. Fin /\ R e. Domn ) -> ( ( Unit ` R ) i^i { ( 0g ` R ) } ) = (/) )
17 1 11 unitss 
 |-  ( Unit ` R ) C_ B
18 reldisj 
 |-  ( ( Unit ` R ) C_ B -> ( ( ( Unit ` R ) i^i { ( 0g ` R ) } ) = (/) <-> ( Unit ` R ) C_ ( B \ { ( 0g ` R ) } ) ) )
19 17 18 ax-mp 
 |-  ( ( ( Unit ` R ) i^i { ( 0g ` R ) } ) = (/) <-> ( Unit ` R ) C_ ( B \ { ( 0g ` R ) } ) )
20 16 19 sylib 
 |-  ( ( B e. Fin /\ R e. Domn ) -> ( Unit ` R ) C_ ( B \ { ( 0g ` R ) } ) )
21 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 simplr 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> R e. Domn )
24 simpll 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> B e. Fin )
25 simpr 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> x e. ( B \ { ( 0g ` R ) } ) )
26 eqid 
 |-  ( y e. B |-> ( y ( .r ` R ) x ) ) = ( y e. B |-> ( y ( .r ` R ) x ) )
27 1 7 6 21 22 23 24 25 26 fidomndrnglem 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> x ( ||r ` R ) ( 1r ` R ) )
28 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
29 28 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
30 28 7 oppr0 
 |-  ( 0g ` R ) = ( 0g ` ( oppR ` R ) )
31 28 6 oppr1 
 |-  ( 1r ` R ) = ( 1r ` ( oppR ` R ) )
32 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
33 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
34 28 opprdomn 
 |-  ( R e. Domn -> ( oppR ` R ) e. Domn )
35 23 34 syl 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> ( oppR ` R ) e. Domn )
36 eqid 
 |-  ( y e. B |-> ( y ( .r ` ( oppR ` R ) ) x ) ) = ( y e. B |-> ( y ( .r ` ( oppR ` R ) ) x ) )
37 29 30 31 32 33 35 24 25 36 fidomndrnglem 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
38 11 6 21 28 32 isunit 
 |-  ( x e. ( Unit ` R ) <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
39 27 37 38 sylanbrc 
 |-  ( ( ( B e. Fin /\ R e. Domn ) /\ x e. ( B \ { ( 0g ` R ) } ) ) -> x e. ( Unit ` R ) )
40 20 39 eqelssd 
 |-  ( ( B e. Fin /\ R e. Domn ) -> ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) )
41 1 11 7 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) ) )
42 3 40 41 sylanbrc 
 |-  ( ( B e. Fin /\ R e. Domn ) -> R e. DivRing )
43 42 ex 
 |-  ( B e. Fin -> ( R e. Domn -> R e. DivRing ) )
44 drngdomn 
 |-  ( R e. DivRing -> R e. Domn )
45 43 44 impbid1 
 |-  ( B e. Fin -> ( R e. Domn <-> R e. DivRing ) )