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	$⊢ φ \to A \in AssAlg$
	assafld.1	$⊢ φ \to A \in IDomn$
	assafld.2	$⊢ φ \to K \in DivRing$
	assafld.3	$⊢ φ \to \dim (A) \in ℕ_{0}$
Assertion	assafld	$⊢ φ \to A \in Field$

Proof

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

Metamath Proof Explorer

Theorem assafld

Proof