issubdrg

Description: Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014)

	Ref	Expression
Hypotheses	issubdrg.s	$⊢ S = R ↾_{𝑠} A$
	issubdrg.z	$⊢ \underset{˙}{0} = 0_{R}$
	issubdrg.i	$⊢ I = {inv}_{r} (R)$
Assertion	issubdrg	$⊢ (R \in DivRing \land A \in SubRing (R)) \to (S \in DivRing \leftrightarrow \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A)$

Proof

Step	Hyp	Ref	Expression
1		issubdrg.s	$⊢ S = R ↾_{𝑠} A$
2		issubdrg.z	$⊢ \underset{˙}{0} = 0_{R}$
3		issubdrg.i	$⊢ I = {inv}_{r} (R)$
4		simpllr	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to A \in SubRing (R)$
5	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
6	4 5	syl	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to S \in Ring$
7		simpr	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in (A ∖ \{\underset{˙}{0}\})$
8		eldifsn	$⊢ x \in (A ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in A \land x \neq \underset{˙}{0})$
9	7 8	sylib	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to (x \in A \land x \neq \underset{˙}{0})$
10	9	simpld	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in A$
11	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
12	4 11	syl	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to A = {Base}_{S}$
13	10 12	eleqtrd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in {Base}_{S}$
14	9	simprd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
15	1 2	subrg0	$⊢ A \in SubRing (R) \to \underset{˙}{0} = 0_{S}$
16	4 15	syl	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} = 0_{S}$
17	14 16	neeqtrd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \neq 0_{S}$
18		eqid	$⊢ {Base}_{S} = {Base}_{S}$
19		eqid	$⊢ Unit (S) = Unit (S)$
20		eqid	$⊢ 0_{S} = 0_{S}$
21	18 19 20	drngunit	$⊢ S \in DivRing \to (x \in Unit (S) \leftrightarrow (x \in {Base}_{S} \land x \neq 0_{S}))$
22	21	ad2antlr	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to (x \in Unit (S) \leftrightarrow (x \in {Base}_{S} \land x \neq 0_{S}))$
23	13 17 22	mpbir2and	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in Unit (S)$
24		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
25	19 24 18	ringinvcl	$⊢ (S \in Ring \land x \in Unit (S)) \to {inv}_{r} (S) (x) \in {Base}_{S}$
26	6 23 25	syl2anc	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to {inv}_{r} (S) (x) \in {Base}_{S}$
27	1 3 19 24	subrginv	$⊢ (A \in SubRing (R) \land x \in Unit (S)) \to I (x) = {inv}_{r} (S) (x)$
28	4 23 27	syl2anc	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to I (x) = {inv}_{r} (S) (x)$
29	26 28 12	3eltr4d	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to I (x) \in A$
30	29	ralrimiva	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \to \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A$
31	5	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to S \in Ring$
32		eqid	$⊢ Unit (R) = Unit (R)$
33	1 32 19	subrguss	$⊢ A \in SubRing (R) \to Unit (S) \subseteq Unit (R)$
34	33	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) \subseteq Unit (R)$
35		eqid	$⊢ {Base}_{R} = {Base}_{R}$
36	35 32 2	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{\underset{˙}{0}\})$
37	36	simprbi	$⊢ R \in DivRing \to Unit (R) = {Base}_{R} ∖ \{\underset{˙}{0}\}$
38	37	ad2antrr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (R) = {Base}_{R} ∖ \{\underset{˙}{0}\}$
39	34 38	sseqtrd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) \subseteq {Base}_{R} ∖ \{\underset{˙}{0}\}$
40	18 19	unitss	$⊢ Unit (S) \subseteq {Base}_{S}$
41	11	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A = {Base}_{S}$
42	40 41	sseqtrrid	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) \subseteq A$
43	39 42	ssind	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) \subseteq ({Base}_{R} ∖ \{\underset{˙}{0}\}) \cap A$
44	35	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
45	44	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A \subseteq {Base}_{R}$
46		difin2	$⊢ A \subseteq {Base}_{R} \to A ∖ \{\underset{˙}{0}\} = ({Base}_{R} ∖ \{\underset{˙}{0}\}) \cap A$
47	45 46	syl	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A ∖ \{\underset{˙}{0}\} = ({Base}_{R} ∖ \{\underset{˙}{0}\}) \cap A$
48	43 47	sseqtrrd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) \subseteq A ∖ \{\underset{˙}{0}\}$
49	44	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to A \subseteq {Base}_{R}$
50		simprl	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in (A ∖ \{\underset{˙}{0}\})$
51	50 8	sylib	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to (x \in A \land x \neq \underset{˙}{0})$
52	51	simpld	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in A$
53	49 52	sseldd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in {Base}_{R}$
54	51	simprd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \neq \underset{˙}{0}$
55	35 32 2	drngunit	$⊢ R \in DivRing \to (x \in Unit (R) \leftrightarrow (x \in {Base}_{R} \land x \neq \underset{˙}{0}))$
56	55	ad2antrr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to (x \in Unit (R) \leftrightarrow (x \in {Base}_{R} \land x \neq \underset{˙}{0}))$
57	53 54 56	mpbir2and	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in Unit (R)$
58		simprr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to I (x) \in A$
59	1 32 19 3	subrgunit	$⊢ A \in SubRing (R) \to (x \in Unit (S) \leftrightarrow (x \in Unit (R) \land x \in A \land I (x) \in A))$
60	59	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to (x \in Unit (S) \leftrightarrow (x \in Unit (R) \land x \in A \land I (x) \in A))$
61	57 52 58 60	mpbir3and	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in Unit (S)$
62	61	expr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land x \in (A ∖ \{\underset{˙}{0}\})) \to (I (x) \in A \to x \in Unit (S))$
63	62	ralimdva	$⊢ (R \in DivRing \land A \in SubRing (R)) \to (\forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A \to \forall x \in (A ∖ \{\underset{˙}{0}\}) x \in Unit (S))$
64	63	imp	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to \forall x \in (A ∖ \{\underset{˙}{0}\}) x \in Unit (S)$
65		dfss3	$⊢ A ∖ \{\underset{˙}{0}\} \subseteq Unit (S) \leftrightarrow \forall x \in (A ∖ \{\underset{˙}{0}\}) x \in Unit (S)$
66	64 65	sylibr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A ∖ \{\underset{˙}{0}\} \subseteq Unit (S)$
67	48 66	eqssd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) = A ∖ \{\underset{˙}{0}\}$
68	15	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to \underset{˙}{0} = 0_{S}$
69	68	sneqd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to \{\underset{˙}{0}\} = \{0_{S}\}$
70	41 69	difeq12d	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A ∖ \{\underset{˙}{0}\} = {Base}_{S} ∖ \{0_{S}\}$
71	67 70	eqtrd	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to Unit (S) = {Base}_{S} ∖ \{0_{S}\}$
72	18 19 20	isdrng	$⊢ S \in DivRing \leftrightarrow (S \in Ring \land Unit (S) = {Base}_{S} ∖ \{0_{S}\})$
73	31 71 72	sylanbrc	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to S \in DivRing$
74	30 73	impbida	$⊢ (R \in DivRing \land A \in SubRing (R)) \to (S \in DivRing \leftrightarrow \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A)$

Metamath Proof Explorer

Theorem issubdrg

Proof