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

Metamath Proof Explorer

Theorem assafld

Description: If an algebra A of finite degree over a division ring K is an integral domain, then it is a field. Corollary of Proposition 2. in Chapter 5. of BourbakiAlg2 p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses assafld.k 
|- K = ( Scalar ` A )
assafld.a 
|- ( ph -> A e. AssAlg )
assafld.1 
|- ( ph -> A e. IDomn )
assafld.2 
|- ( ph -> K e. DivRing )
assafld.3 
|- ( ph -> ( dim ` A ) e. NN0 )
Assertion assafld 
|- ( ph -> A e. Field )

Proof

Step Hyp Ref Expression
1 assafld.k 
 |-  K = ( Scalar ` A )
2 assafld.a 
 |-  ( ph -> A e. AssAlg )
3 assafld.1 
 |-  ( ph -> A e. IDomn )
4 assafld.2 
 |-  ( ph -> K e. DivRing )
5 assafld.3 
 |-  ( ph -> ( dim ` A ) e. NN0 )
6 3 idomringd 
 |-  ( ph -> A e. Ring )
7 eqid 
 |-  ( Base ` A ) = ( Base ` A )
8 eqid 
 |-  ( Unit ` A ) = ( Unit ` A )
9 7 8 unitss 
 |-  ( Unit ` A ) C_ ( Base ` A )
10 9 a1i 
 |-  ( ph -> ( Unit ` A ) C_ ( Base ` A ) )
11 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
12 3 idomdomd 
 |-  ( ph -> A e. Domn )
13 domnnzr 
 |-  ( A e. Domn -> A e. NzRing )
14 12 13 syl 
 |-  ( ph -> A e. NzRing )
15 14 adantr 
 |-  ( ( ph /\ ( 0g ` A ) e. ( Unit ` A ) ) -> A e. NzRing )
16 simpr 
 |-  ( ( ph /\ ( 0g ` A ) e. ( Unit ` A ) ) -> ( 0g ` A ) e. ( Unit ` A ) )
17 8 11 15 16 unitnz 
 |-  ( ( ph /\ ( 0g ` A ) e. ( Unit ` A ) ) -> ( 0g ` A ) =/= ( 0g ` A ) )
18 neirr 
 |-  -. ( 0g ` A ) =/= ( 0g ` A )
19 18 a1i 
 |-  ( ( ph /\ ( 0g ` A ) e. ( Unit ` A ) ) -> -. ( 0g ` A ) =/= ( 0g ` A ) )
20 17 19 pm2.65da 
 |-  ( ph -> -. ( 0g ` A ) e. ( Unit ` A ) )
21 ssdifsn 
 |-  ( ( Unit ` A ) C_ ( ( Base ` A ) \ { ( 0g ` A ) } ) <-> ( ( Unit ` A ) C_ ( Base ` A ) /\ -. ( 0g ` A ) e. ( Unit ` A ) ) )
22 10 20 21 sylanbrc 
 |-  ( ph -> ( Unit ` A ) C_ ( ( Base ` A ) \ { ( 0g ` A ) } ) )
23 eqid 
 |-  ( RLReg ` A ) = ( RLReg ` A )
24 2 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> A e. AssAlg )
25 4 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> K e. DivRing )
26 5 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> ( dim ` A ) e. NN0 )
27 12 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> A e. Domn )
28 simpr 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) )
29 28 eldifad 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> x e. ( Base ` A ) )
30 eldifsni 
 |-  ( x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) -> x =/= ( 0g ` A ) )
31 28 30 syl 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> x =/= ( 0g ` A ) )
32 7 23 11 domnrrg 
 |-  ( ( A e. Domn /\ x e. ( Base ` A ) /\ x =/= ( 0g ` A ) ) -> x e. ( RLReg ` A ) )
33 27 29 31 32 syl3anc 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> x e. ( RLReg ` A ) )
34 23 8 1 24 25 26 33 assarrginv 
 |-  ( ( ph /\ x e. ( ( Base ` A ) \ { ( 0g ` A ) } ) ) -> x e. ( Unit ` A ) )
35 22 34 eqelssd 
 |-  ( ph -> ( Unit ` A ) = ( ( Base ` A ) \ { ( 0g ` A ) } ) )
36 7 8 11 isdrng 
 |-  ( A e. DivRing <-> ( A e. Ring /\ ( Unit ` A ) = ( ( Base ` A ) \ { ( 0g ` A ) } ) ) )
37 6 35 36 sylanbrc 
 |-  ( ph -> A e. DivRing )
38 3 idomcringd 
 |-  ( ph -> A e. CRing )
39 isfld 
 |-  ( A e. Field <-> ( A e. DivRing /\ A e. CRing ) )
40 37 38 39 sylanbrc 
 |-  ( ph -> A e. Field )