# Metamath Proof Explorer

## Theorem fidomndrng

Description: A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis fidomndrng.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion fidomndrng ${⊢}{B}\in \mathrm{Fin}\to \left({R}\in \mathrm{Domn}↔{R}\in \mathrm{DivRing}\right)$

### Proof

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