sdrgacs

Description: Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015)

		Ref	Expression
	Hypothesis	subrgacs.b	$⊢ B = {Base}_{R}$
	Assertion	sdrgacs	$⊢ R \in DivRing \to SubDRing (R) \in ACS (B)$

Proof

Step	Hyp	Ref	Expression
1		subrgacs.b	$⊢ B = {Base}_{R}$
2		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
3		eqid	$⊢ 0_{R} = 0_{R}$
4	2 3	issdrg2	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s)$
5		3anass	$⊢ (R \in DivRing \land s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s) \leftrightarrow (R \in DivRing \land (s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s))$
6	4 5	bitri	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land (s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s))$
7	6	baib	$⊢ R \in DivRing \to (s \in SubDRing (R) \leftrightarrow (s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s))$
8	1	subrgss	$⊢ s \in SubRing (R) \to s \subseteq B$
9		velpw	$⊢ s \in 𝒫 B \leftrightarrow s \subseteq B$
10	8 9	sylibr	$⊢ s \in SubRing (R) \to s \in 𝒫 B$
11	10	adantl	$⊢ (R \in DivRing \land s \in SubRing (R)) \to s \in 𝒫 B$
12		iftrue	$⊢ x = 0_{R} \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) = x$
13	12	eleq1d	$⊢ x = 0_{R} \to (if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y \leftrightarrow x \in y)$
14	13	biimprd	$⊢ x = 0_{R} \to (x \in y \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y)$
15		eldifsni	$⊢ x \in (y ∖ \{0_{R}\}) \to x \neq 0_{R}$
16	15	necon2bi	$⊢ x = 0_{R} \to \neg x \in (y ∖ \{0_{R}\})$
17	16	pm2.21d	$⊢ x = 0_{R} \to (x \in (y ∖ \{0_{R}\}) \to {inv}_{r} (R) (x) \in y)$
18	14 17	2thd	$⊢ x = 0_{R} \to ((x \in y \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y) \leftrightarrow (x \in (y ∖ \{0_{R}\}) \to {inv}_{r} (R) (x) \in y))$
19		eldifsn	$⊢ x \in (y ∖ \{0_{R}\}) \leftrightarrow (x \in y \land x \neq 0_{R})$
20	19	rbaibr	$⊢ x \neq 0_{R} \to (x \in y \leftrightarrow x \in (y ∖ \{0_{R}\}))$
21		ifnefalse	$⊢ x \neq 0_{R} \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) = {inv}_{r} (R) (x)$
22	21	eleq1d	$⊢ x \neq 0_{R} \to (if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y \leftrightarrow {inv}_{r} (R) (x) \in y)$
23	20 22	imbi12d	$⊢ x \neq 0_{R} \to ((x \in y \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y) \leftrightarrow (x \in (y ∖ \{0_{R}\}) \to {inv}_{r} (R) (x) \in y))$
24	18 23	pm2.61ine	$⊢ (x \in y \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y) \leftrightarrow (x \in (y ∖ \{0_{R}\}) \to {inv}_{r} (R) (x) \in y)$
25	24	ralbii2	$⊢ \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y \leftrightarrow \forall x \in (y ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in y$
26		difeq1	$⊢ y = s \to y ∖ \{0_{R}\} = s ∖ \{0_{R}\}$
27		eleq2w	$⊢ y = s \to ({inv}_{r} (R) (x) \in y \leftrightarrow {inv}_{r} (R) (x) \in s)$
28	26 27	raleqbidv	$⊢ y = s \to (\forall x \in (y ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in y \leftrightarrow \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s)$
29	25 28	syl5bb	$⊢ y = s \to (\forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y \leftrightarrow \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s)$
30	29	elrab3	$⊢ s \in 𝒫 B \to (s \in \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \leftrightarrow \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s)$
31	11 30	syl	$⊢ (R \in DivRing \land s \in SubRing (R)) \to (s \in \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \leftrightarrow \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s)$
32	31	pm5.32da	$⊢ R \in DivRing \to ((s \in SubRing (R) \land s \in \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\}) \leftrightarrow (s \in SubRing (R) \land \forall x \in (s ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in s))$
33	7 32	bitr4d	$⊢ R \in DivRing \to (s \in SubDRing (R) \leftrightarrow (s \in SubRing (R) \land s \in \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\}))$
34		elin	$⊢ s \in (SubRing (R) \cap \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\}) \leftrightarrow (s \in SubRing (R) \land s \in \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\})$
35	33 34	bitr4di	$⊢ R \in DivRing \to (s \in SubDRing (R) \leftrightarrow s \in (SubRing (R) \cap \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\}))$
36	35	eqrdv	$⊢ R \in DivRing \to SubDRing (R) = SubRing (R) \cap \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\}$
37	1	fvexi	$⊢ B \in V$
38		mreacs	$⊢ B \in V \to ACS (B) \in Moore (𝒫 B)$
39	37 38	mp1i	$⊢ R \in DivRing \to ACS (B) \in Moore (𝒫 B)$
40		drngring	$⊢ R \in DivRing \to R \in Ring$
41	1	subrgacs	$⊢ R \in Ring \to SubRing (R) \in ACS (B)$
42	40 41	syl	$⊢ R \in DivRing \to SubRing (R) \in ACS (B)$
43		simplr	$⊢ ((R \in DivRing \land x \in B) \land x = 0_{R}) \to x \in B$
44		df-ne	$⊢ x \neq 0_{R} \leftrightarrow \neg x = 0_{R}$
45	1 3 2	drnginvrcl	$⊢ (R \in DivRing \land x \in B \land x \neq 0_{R}) \to {inv}_{r} (R) (x) \in B$
46	45	3expa	$⊢ ((R \in DivRing \land x \in B) \land x \neq 0_{R}) \to {inv}_{r} (R) (x) \in B$
47	44 46	sylan2br	$⊢ ((R \in DivRing \land x \in B) \land \neg x = 0_{R}) \to {inv}_{r} (R) (x) \in B$
48	43 47	ifclda	$⊢ (R \in DivRing \land x \in B) \to if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in B$
49	48	ralrimiva	$⊢ R \in DivRing \to \forall x \in B if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in B$
50		acsfn1	$⊢ (B \in V \land \forall x \in B if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in B) \to \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \in ACS (B)$
51	37 49 50	sylancr	$⊢ R \in DivRing \to \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \in ACS (B)$
52		mreincl	$⊢ (ACS (B) \in Moore (𝒫 B) \land SubRing (R) \in ACS (B) \land \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \in ACS (B)) \to SubRing (R) \cap \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \in ACS (B)$
53	39 42 51 52	syl3anc	$⊢ R \in DivRing \to SubRing (R) \cap \{y \in 𝒫 B \| \forall x \in y if (x = 0_{R}, x, {inv}_{r} (R) (x)) \in y\} \in ACS (B)$
54	36 53	eqeltrd	$⊢ R \in DivRing \to SubDRing (R) \in ACS (B)$

Metamath Proof Explorer

Theorem sdrgacs

Proof