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 ⊢ 𝐾 = ( Scalar ‘ 𝐴 )
assafld.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
assafld.1 ⊢ ( 𝜑 → 𝐴 ∈ IDomn )
assafld.2 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
assafld.3 ⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
Assertion assafld ( 𝜑 → 𝐴 ∈ Field )

Proof

Step Hyp Ref Expression
1 assafld.k ⊢ 𝐾 = ( Scalar ‘ 𝐴 )
2 assafld.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
3 assafld.1 ⊢ ( 𝜑 → 𝐴 ∈ IDomn )
4 assafld.2 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
5 assafld.3 ⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
6 3 idomringd ⊢ ( 𝜑 → 𝐴 ∈ Ring )
7 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
8 eqid ⊢ ( Unit ‘ 𝐴 ) = ( Unit ‘ 𝐴 )
9 7 8 unitss ⊢ ( Unit ‘ 𝐴 ) ⊆ ( Base ‘ 𝐴 )
10 9 a1i ⊢ ( 𝜑 → ( Unit ‘ 𝐴 ) ⊆ ( Base ‘ 𝐴 ) )
11 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
12 3 idomdomd ⊢ ( 𝜑 → 𝐴 ∈ Domn )
13 domnnzr ⊢ ( 𝐴 ∈ Domn → 𝐴 ∈ NzRing )
14 12 13 syl ⊢ ( 𝜑 → 𝐴 ∈ NzRing )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) ) → 𝐴 ∈ NzRing )
16 simpr ⊢ ( ( 𝜑 ∧ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) ) → ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) )
17 8 11 15 16 unitnz ⊢ ( ( 𝜑 ∧ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) ) → ( 0g ‘ 𝐴 ) ≠ ( 0g ‘ 𝐴 ) )
18 neirr ⊢ ¬ ( 0g ‘ 𝐴 ) ≠ ( 0g ‘ 𝐴 )
19 18 a1i ⊢ ( ( 𝜑 ∧ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) ) → ¬ ( 0g ‘ 𝐴 ) ≠ ( 0g ‘ 𝐴 ) )
20 17 19 pm2.65da ⊢ ( 𝜑 → ¬ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) )
21 ssdifsn ⊢ ( ( Unit ‘ 𝐴 ) ⊆ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ↔ ( ( Unit ‘ 𝐴 ) ⊆ ( Base ‘ 𝐴 ) ∧ ¬ ( 0g ‘ 𝐴 ) ∈ ( Unit ‘ 𝐴 ) ) )
22 10 20 21 sylanbrc ⊢ ( 𝜑 → ( Unit ‘ 𝐴 ) ⊆ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) )
23 eqid ⊢ ( RLReg ‘ 𝐴 ) = ( RLReg ‘ 𝐴 )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝐴 ∈ AssAlg )
25 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝐾 ∈ DivRing )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → ( dim ‘ 𝐴 ) ∈ ℕ0 )
27 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝐴 ∈ Domn )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) )
29 28 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
30 eldifsni ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) → 𝑥 ≠ ( 0g ‘ 𝐴 ) )
31 28 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝑥 ≠ ( 0g ‘ 𝐴 ) )
32 7 23 11 domnrrg ⊢ ( ( 𝐴 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑥 ≠ ( 0g ‘ 𝐴 ) ) → 𝑥 ∈ ( RLReg ‘ 𝐴 ) )
33 27 29 31 32 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝑥 ∈ ( RLReg ‘ 𝐴 ) )
34 23 8 1 24 25 26 33 assarrginv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) → 𝑥 ∈ ( Unit ‘ 𝐴 ) )
35 22 34 eqelssd ⊢ ( 𝜑 → ( Unit ‘ 𝐴 ) = ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) )
36 7 8 11 isdrng ⊢ ( 𝐴 ∈ DivRing ↔ ( 𝐴 ∈ Ring ∧ ( Unit ‘ 𝐴 ) = ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) )
37 6 35 36 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ DivRing )
38 3 idomcringd ⊢ ( 𝜑 → 𝐴 ∈ CRing )
39 isfld ⊢ ( 𝐴 ∈ Field ↔ ( 𝐴 ∈ DivRing ∧ 𝐴 ∈ CRing ) )
40 37 38 39 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ Field )