This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )