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 )