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 \in Fin \to (R \in Domn \leftrightarrow R \in DivRing)$

Proof

Step	Hyp	Ref	Expression
1		fidomndrng.b	$⊢ B = {Base}_{R}$
2		domnring	$⊢ R \in Domn \to R \in Ring$
3	2	adantl	$⊢ (B \in Fin \land R \in Domn) \to R \in Ring$
4		domnnzr	$⊢ R \in Domn \to R \in NzRing$
5	4	adantl	$⊢ (B \in Fin \land R \in Domn) \to R \in NzRing$
6		eqid	$⊢ 1_{R} = 1_{R}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	6 7	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
9	5 8	syl	$⊢ (B \in Fin \land R \in Domn) \to 1_{R} \neq 0_{R}$
10	9	neneqd	$⊢ (B \in Fin \land R \in Domn) \to \neg 1_{R} = 0_{R}$
11		eqid	$⊢ Unit (R) = Unit (R)$
12	11 7 6	0unit	$⊢ R \in Ring \to (0_{R} \in Unit (R) \leftrightarrow 1_{R} = 0_{R})$
13	3 12	syl	$⊢ (B \in Fin \land R \in Domn) \to (0_{R} \in Unit (R) \leftrightarrow 1_{R} = 0_{R})$
14	10 13	mtbird	$⊢ (B \in Fin \land R \in Domn) \to \neg 0_{R} \in Unit (R)$
15		disjsn	$⊢ Unit (R) \cap \{0_{R}\} = \emptyset \leftrightarrow \neg 0_{R} \in Unit (R)$
16	14 15	sylibr	$⊢ (B \in Fin \land R \in Domn) \to Unit (R) \cap \{0_{R}\} = \emptyset$
17	1 11	unitss	$⊢ Unit (R) \subseteq B$
18		reldisj	$⊢ Unit (R) \subseteq B \to (Unit (R) \cap \{0_{R}\} = \emptyset \leftrightarrow Unit (R) \subseteq B ∖ \{0_{R}\})$
19	17 18	ax-mp	$⊢ Unit (R) \cap \{0_{R}\} = \emptyset \leftrightarrow Unit (R) \subseteq B ∖ \{0_{R}\}$
20	16 19	sylib	$⊢ (B \in Fin \land R \in Domn) \to Unit (R) \subseteq B ∖ \{0_{R}\}$
21		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23		simplr	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to R \in Domn$
24		simpll	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to B \in Fin$
25		simpr	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to x \in (B ∖ \{0_{R}\})$
26		eqid	$⊢ (y \in B ⟼ y \cdot_{R} x) = (y \in B ⟼ y \cdot_{R} x)$
27	1 7 6 21 22 23 24 25 26	fidomndrnglem	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to x ∥_{r} (R) 1_{R}$
28		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
29	28 1	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
30	28 7	oppr0	$⊢ 0_{R} = 0_{{opp}_{r} (R)}$
31	28 6	oppr1	$⊢ 1_{R} = 1_{{opp}_{r} (R)}$
32		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
33		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
34	28	opprdomn	$⊢ R \in Domn \to {opp}_{r} (R) \in Domn$
35	23 34	syl	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to {opp}_{r} (R) \in Domn$
36		eqid	$⊢ (y \in B ⟼ y \cdot_{{opp}_{r} (R)} x) = (y \in B ⟼ y \cdot_{{opp}_{r} (R)} x)$
37	29 30 31 32 33 35 24 25 36	fidomndrnglem	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to x ∥_{r} ({opp}_{r} (R)) 1_{R}$
38	11 6 21 28 32	isunit	$⊢ x \in Unit (R) \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
39	27 37 38	sylanbrc	$⊢ ((B \in Fin \land R \in Domn) \land x \in (B ∖ \{0_{R}\})) \to x \in Unit (R)$
40	20 39	eqelssd	$⊢ (B \in Fin \land R \in Domn) \to Unit (R) = B ∖ \{0_{R}\}$
41	1 11 7	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{0_{R}\})$
42	3 40 41	sylanbrc	$⊢ (B \in Fin \land R \in Domn) \to R \in DivRing$
43	42	ex	$⊢ B \in Fin \to (R \in Domn \to R \in DivRing)$
44		drngdomn	$⊢ R \in DivRing \to R \in Domn$
45	43 44	impbid1	$⊢ B \in Fin \to (R \in Domn \leftrightarrow R \in DivRing)$

Metamath Proof Explorer

Theorem fidomndrng

Proof