isdomn3

Description: Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015)

	Ref	Expression
Hypotheses	isdomn3.b	$⊢ B = {Base}_{R}$
	isdomn3.z	$⊢ \underset{˙}{0} = 0_{R}$
	isdomn3.u	$⊢ U = {mulGrp}_{R}$
Assertion	isdomn3	$⊢ R \in Domn \leftrightarrow (R \in Ring \land B ∖ \{\underset{˙}{0}\} \in SubMnd (U))$

Proof

Step	Hyp	Ref	Expression
1		isdomn3.b	$⊢ B = {Base}_{R}$
2		isdomn3.z	$⊢ \underset{˙}{0} = 0_{R}$
3		isdomn3.u	$⊢ U = {mulGrp}_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5	1 4 2	isdomn	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	6 2	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq \underset{˙}{0})$
8	7	anbi1i	$⊢ (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow ((R \in Ring \land 1_{R} \neq \underset{˙}{0}) \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))$
9		anass	$⊢ ((R \in Ring \land 1_{R} \neq \underset{˙}{0}) \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow (R \in Ring \land (1_{R} \neq \underset{˙}{0} \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
10	8 9	bitri	$⊢ (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow (R \in Ring \land (1_{R} \neq \underset{˙}{0} \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))))$
11	1 6	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
12		eldifsn	$⊢ 1_{R} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (1_{R} \in B \land 1_{R} \neq \underset{˙}{0})$
13	12	baibr	$⊢ 1_{R} \in B \to (1_{R} \neq \underset{˙}{0} \leftrightarrow 1_{R} \in (B ∖ \{\underset{˙}{0}\}))$
14	11 13	syl	$⊢ R \in Ring \to (1_{R} \neq \underset{˙}{0} \leftrightarrow 1_{R} \in (B ∖ \{\underset{˙}{0}\}))$
15	1 4	ringcl	$⊢ (R \in Ring \land x \in B \land y \in B) \to x \cdot_{R} y \in B$
16	15	3expb	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to x \cdot_{R} y \in B$
17	16	biantrurd	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to (x \cdot_{R} y \neq \underset{˙}{0} \leftrightarrow (x \cdot_{R} y \in B \land x \cdot_{R} y \neq \underset{˙}{0}))$
18		eldifsn	$⊢ x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \cdot_{R} y \in B \land x \cdot_{R} y \neq \underset{˙}{0})$
19	17 18	bitr4di	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to (x \cdot_{R} y \neq \underset{˙}{0} \leftrightarrow x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
20	19	imbi2d	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to (((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \neq \underset{˙}{0}) \leftrightarrow ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
21	20	2ralbidva	$⊢ R \in Ring \to (\forall x \in B \forall y \in B ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \neq \underset{˙}{0}) \leftrightarrow \forall x \in B \forall y \in B ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
22		con34b	$⊢ (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow (\neg (x = \underset{˙}{0} \lor y = \underset{˙}{0}) \to \neg x \cdot_{R} y = \underset{˙}{0})$
23		neanior	$⊢ (x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \leftrightarrow \neg (x = \underset{˙}{0} \lor y = \underset{˙}{0})$
24		df-ne	$⊢ x \cdot_{R} y \neq \underset{˙}{0} \leftrightarrow \neg x \cdot_{R} y = \underset{˙}{0}$
25	23 24	imbi12i	$⊢ ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \neq \underset{˙}{0}) \leftrightarrow (\neg (x = \underset{˙}{0} \lor y = \underset{˙}{0}) \to \neg x \cdot_{R} y = \underset{˙}{0})$
26	22 25	bitr4i	$⊢ (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \neq \underset{˙}{0})$
27	26	2ralbii	$⊢ \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow \forall x \in B \forall y \in B ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \neq \underset{˙}{0})$
28		impexp	$⊢ (((x \in B \land y \in B) \land (x \neq \underset{˙}{0} \land y \neq \underset{˙}{0})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow ((x \in B \land y \in B) \to ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
29		an4	$⊢ ((x \in B \land y \in B) \land (x \neq \underset{˙}{0} \land y \neq \underset{˙}{0})) \leftrightarrow ((x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0}))$
30		eldifsn	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in B \land x \neq \underset{˙}{0})$
31		eldifsn	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (y \in B \land y \neq \underset{˙}{0})$
32	30 31	anbi12i	$⊢ (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow ((x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0}))$
33	29 32	bitr4i	$⊢ ((x \in B \land y \in B) \land (x \neq \underset{˙}{0} \land y \neq \underset{˙}{0})) \leftrightarrow (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))$
34	33	imbi1i	$⊢ (((x \in B \land y \in B) \land (x \neq \underset{˙}{0} \land y \neq \underset{˙}{0})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow ((x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
35	28 34	bitr3i	$⊢ ((x \in B \land y \in B) \to ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))) \leftrightarrow ((x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
36	35	2albii	$⊢ \forall x \forall y ((x \in B \land y \in B) \to ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))) \leftrightarrow \forall x \forall y ((x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
37		r2al	$⊢ \forall x \in B \forall y \in B ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow \forall x \forall y ((x \in B \land y \in B) \to ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
38		r2al	$⊢ \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow \forall x \forall y ((x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
39	36 37 38	3bitr4ri	$⊢ \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow \forall x \in B \forall y \in B ((x \neq \underset{˙}{0} \land y \neq \underset{˙}{0}) \to x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
40	21 27 39	3bitr4g	$⊢ R \in Ring \to (\forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})) \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))$
41	14 40	anbi12d	$⊢ R \in Ring \to ((1_{R} \neq \underset{˙}{0} \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
42	3	ringmgp	$⊢ R \in Ring \to U \in Mnd$
43	3 1	mgpbas	$⊢ B = {Base}_{U}$
44	3 6	ringidval	$⊢ 1_{R} = 0_{U}$
45	3 4	mgpplusg	$⊢ \cdot_{R} = +_{U}$
46	43 44 45	issubm	$⊢ U \in Mnd \to (B ∖ \{\underset{˙}{0}\} \in SubMnd (U) \leftrightarrow (B ∖ \{\underset{˙}{0}\} \subseteq B \land 1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
47		3anass	$⊢ (B ∖ \{\underset{˙}{0}\} \subseteq B \land 1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow (B ∖ \{\underset{˙}{0}\} \subseteq B \land (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
48	46 47	syl6bb	$⊢ U \in Mnd \to (B ∖ \{\underset{˙}{0}\} \in SubMnd (U) \leftrightarrow (B ∖ \{\underset{˙}{0}\} \subseteq B \land (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\}))))$
49		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
50	49	biantrur	$⊢ (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})) \leftrightarrow (B ∖ \{\underset{˙}{0}\} \subseteq B \land (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
51	48 50	bitr4di	$⊢ U \in Mnd \to (B ∖ \{\underset{˙}{0}\} \in SubMnd (U) \leftrightarrow (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
52	42 51	syl	$⊢ R \in Ring \to (B ∖ \{\underset{˙}{0}\} \in SubMnd (U) \leftrightarrow (1_{R} \in (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) x \cdot_{R} y \in (B ∖ \{\underset{˙}{0}\})))$
53	41 52	bitr4d	$⊢ R \in Ring \to ((1_{R} \neq \underset{˙}{0} \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow B ∖ \{\underset{˙}{0}\} \in SubMnd (U))$
54	53	pm5.32i	$⊢ (R \in Ring \land (1_{R} \neq \underset{˙}{0} \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0})))) \leftrightarrow (R \in Ring \land B ∖ \{\underset{˙}{0}\} \in SubMnd (U))$
55	10 54	bitri	$⊢ (R \in NzRing \land \forall x \in B \forall y \in B (x \cdot_{R} y = \underset{˙}{0} \to (x = \underset{˙}{0} \lor y = \underset{˙}{0}))) \leftrightarrow (R \in Ring \land B ∖ \{\underset{˙}{0}\} \in SubMnd (U))$
56	5 55	bitri	$⊢ R \in Domn \leftrightarrow (R \in Ring \land B ∖ \{\underset{˙}{0}\} \in SubMnd (U))$

Metamath Proof Explorer

Theorem isdomn3

Proof