Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	fidomndrng	⊢ ( 𝐵 ∈ Fin → ( 𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing ) )

Proof

Step	Hyp	Ref	Expression
1		fidomndrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
3	2	adantl	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → 𝑅 ∈ Ring )
4		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
5	4	adantl	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → 𝑅 ∈ NzRing )
6		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8	6 7	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
9	5 8	syl	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
10	9	neneqd	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ¬ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
11		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
12	11 7 6	0unit	⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
13	3 12	syl	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ( ( 0g ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
14	10 13	mtbird	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ¬ ( 0g ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
15		disjsn	⊢ ( ( ( Unit ‘ 𝑅 ) ∩ { ( 0g ‘ 𝑅 ) } ) = ∅ ↔ ¬ ( 0g ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
16	14 15	sylibr	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ( ( Unit ‘ 𝑅 ) ∩ { ( 0g ‘ 𝑅 ) } ) = ∅ )
17	1 11	unitss	⊢ ( Unit ‘ 𝑅 ) ⊆ 𝐵
18		reldisj	⊢ ( ( Unit ‘ 𝑅 ) ⊆ 𝐵 → ( ( ( Unit ‘ 𝑅 ) ∩ { ( 0g ‘ 𝑅 ) } ) = ∅ ↔ ( Unit ‘ 𝑅 ) ⊆ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) )
19	17 18	ax-mp	⊢ ( ( ( Unit ‘ 𝑅 ) ∩ { ( 0g ‘ 𝑅 ) } ) = ∅ ↔ ( Unit ‘ 𝑅 ) ⊆ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
20	16 19	sylib	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ( Unit ‘ 𝑅 ) ⊆ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
21		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
22		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23		simplr	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑅 ∈ Domn )
24		simpll	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝐵 ∈ Fin )
25		simpr	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
26		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
27	1 7 6 21 22 23 24 25 26	fidomndrnglem	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
28		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
29	28 1	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
30	28 7	oppr0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
31	28 6	oppr1	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) )
32		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
33		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
34	28	opprdomn	⊢ ( 𝑅 ∈ Domn → ( oppr ‘ 𝑅 ) ∈ Domn )
35	23 34	syl	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → ( oppr ‘ 𝑅 ) ∈ Domn )
36		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
37	29 30 31 32 33 35 24 25 36	fidomndrnglem	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
38	11 6 21 28 32	isunit	⊢ ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
39	27 37 38	sylanbrc	⊢ ( ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) ∧ 𝑥 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
40	20 39	eqelssd	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
41	1 11 7	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ) )
42	3 40 41	sylanbrc	⊢ ( ( 𝐵 ∈ Fin ∧ 𝑅 ∈ Domn ) → 𝑅 ∈ DivRing )
43	42	ex	⊢ ( 𝐵 ∈ Fin → ( 𝑅 ∈ Domn → 𝑅 ∈ DivRing ) )
44		drngdomn	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
45	43 44	impbid1	⊢ ( 𝐵 ∈ Fin → ( 𝑅 ∈ Domn ↔ 𝑅 ∈ DivRing ) )