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		eldifsn	$⊢ x \in (A ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in A \land x \neq \underset{˙}{0})$
8	7	bilani	$⊢ (((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})$
9	8	simpld	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in A$
10	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
11	4 10	syl	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to A = {Base}_{S}$
12	9 11	eleqtrd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in {Base}_{S}$
13	8	simprd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
14	1 2	subrg0	$⊢ A \in SubRing (R) \to \underset{˙}{0} = 0_{S}$
15	4 14	syl	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} = 0_{S}$
16	13 15	neeqtrd	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \neq 0_{S}$
17		eqid	$⊢ {Base}_{S} = {Base}_{S}$
18		eqid	$⊢ Unit (S) = Unit (S)$
19		eqid	$⊢ 0_{S} = 0_{S}$
20	17 18 19	drngunit	$⊢ S \in DivRing \to (x \in Unit (S) \leftrightarrow (x \in {Base}_{S} \land x \neq 0_{S}))$
21	20	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}))$
22	12 16 21	mpbir2and	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to x \in Unit (S)$
23		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
24	18 23 17	ringinvcl	$⊢ (S \in Ring \land x \in Unit (S)) \to {inv}_{r} (S) (x) \in {Base}_{S}$
25	6 22 24	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}$
26	1 3 18 23	subrginv	$⊢ (A \in SubRing (R) \land x \in Unit (S)) \to I (x) = {inv}_{r} (S) (x)$
27	4 22 26	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)$
28	25 27 11	3eltr4d	$⊢ (((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \land x \in (A ∖ \{\underset{˙}{0}\})) \to I (x) \in A$
29	28	ralrimiva	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land S \in DivRing) \to \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A$
30	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$
31		eqid	$⊢ Unit (R) = Unit (R)$
32	1 31 18	subrguss	$⊢ A \in SubRing (R) \to Unit (S) \subseteq Unit (R)$
33	32	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)$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35	34 31 2	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{\underset{˙}{0}\})$
36	35	simprbi	$⊢ R \in DivRing \to Unit (R) = {Base}_{R} ∖ \{\underset{˙}{0}\}$
37	36	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}\}$
38	33 37	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}\}$
39	17 18	unitss	$⊢ Unit (S) \subseteq {Base}_{S}$
40	10	ad2antlr	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to A = {Base}_{S}$
41	39 40	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$
42	38 41	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$
43	34	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
44	43	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}$
45		difin2	$⊢ A \subseteq {Base}_{R} \to A ∖ \{\underset{˙}{0}\} = ({Base}_{R} ∖ \{\underset{˙}{0}\}) \cap A$
46	44 45	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$
47	42 46	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}\}$
48	43	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}$
49		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}\})$
50	49 7	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})$
51	50	simpld	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land (x \in (A ∖ \{\underset{˙}{0}\}) \land I (x) \in A)) \to x \in A$
52	48 51	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}$
53	50	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}$
54	34 31 2	drngunit	$⊢ R \in DivRing \to (x \in Unit (R) \leftrightarrow (x \in {Base}_{R} \land x \neq \underset{˙}{0}))$
55	54	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}))$
56	52 53 55	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)$
57		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$
58	1 31 18 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))$
59	58	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))$
60	56 51 57 59	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)$
61	60	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))$
62	61	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))$
63	62	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)$
64		dfss3	$⊢ A ∖ \{\underset{˙}{0}\} \subseteq Unit (S) \leftrightarrow \forall x \in (A ∖ \{\underset{˙}{0}\}) x \in Unit (S)$
65	63 64	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)$
66	47 65	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}\}$
67	14	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}$
68	67	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}\}$
69	40 68	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}\}$
70	66 69	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}\}$
71	17 18 19	isdrng	$⊢ S \in DivRing \leftrightarrow (S \in Ring \land Unit (S) = {Base}_{S} ∖ \{0_{S}\})$
72	30 70 71	sylanbrc	$⊢ ((R \in DivRing \land A \in SubRing (R)) \land \forall x \in (A ∖ \{\underset{˙}{0}\}) I (x) \in A) \to S \in DivRing$
73	29 72	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