mplsubglem

Description: If A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)

	Ref	Expression
Hypotheses	mplsubglem.s	$⊢ S = I mPwSer R$
	mplsubglem.b	$⊢ B = {Base}_{S}$
	mplsubglem.z	$⊢ \underset{˙}{0} = 0_{R}$
	mplsubglem.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplsubglem.i	$⊢ φ \to I \in W$
	mplsubglem.0	$⊢ φ \to \emptyset \in A$
	mplsubglem.a	$⊢ (φ \land (x \in A \land y \in A)) \to x \cup y \in A$
	mplsubglem.y	$⊢ (φ \land (x \in A \land y \subseteq x)) \to y \in A$
	mplsubglem.u	$⊢ φ \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
	mplsubglem.r	$⊢ φ \to R \in Grp$
Assertion	mplsubglem	$⊢ φ \to U \in SubGrp (S)$

Proof

Step	Hyp	Ref	Expression
1		mplsubglem.s	$⊢ S = I mPwSer R$
2		mplsubglem.b	$⊢ B = {Base}_{S}$
3		mplsubglem.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mplsubglem.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		mplsubglem.i	$⊢ φ \to I \in W$
6		mplsubglem.0	$⊢ φ \to \emptyset \in A$
7		mplsubglem.a	$⊢ (φ \land (x \in A \land y \in A)) \to x \cup y \in A$
8		mplsubglem.y	$⊢ (φ \land (x \in A \land y \subseteq x)) \to y \in A$
9		mplsubglem.u	$⊢ φ \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
10		mplsubglem.r	$⊢ φ \to R \in Grp$
11		ssrab2	$⊢ \{g \in B \| g supp \underset{˙}{0} \in A\} \subseteq B$
12	9 11	eqsstrdi	$⊢ φ \to U \subseteq B$
13	1 5 10 4 3 2	psr0cl	$⊢ φ \to D \times \{\underset{˙}{0}\} \in B$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	14 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in {Base}_{R}$
16		fconst6g	$⊢ \underset{˙}{0} \in {Base}_{R} \to (D \times \{\underset{˙}{0}\}) : D ⟶ {Base}_{R}$
17	10 15 16	3syl	$⊢ φ \to (D \times \{\underset{˙}{0}\}) : D ⟶ {Base}_{R}$
18		eldifi	$⊢ u \in (D ∖ \emptyset) \to u \in D$
19	3	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	fvconst2	$⊢ u \in D \to (D \times \{\underset{˙}{0}\}) (u) = \underset{˙}{0}$
21	18 20	syl	$⊢ u \in (D ∖ \emptyset) \to (D \times \{\underset{˙}{0}\}) (u) = \underset{˙}{0}$
22	21	adantl	$⊢ (φ \land u \in (D ∖ \emptyset)) \to (D \times \{\underset{˙}{0}\}) (u) = \underset{˙}{0}$
23	17 22	suppss	$⊢ φ \to (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \subseteq \emptyset$
24		ss0	$⊢ (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \subseteq \emptyset \to (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} = \emptyset$
25	23 24	syl	$⊢ φ \to (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} = \emptyset$
26	25 6	eqeltrd	$⊢ φ \to (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \in A$
27	9	eleq2d	$⊢ φ \to (D \times \{\underset{˙}{0}\} \in U \leftrightarrow D \times \{\underset{˙}{0}\} \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
28		oveq1	$⊢ g = D \times \{\underset{˙}{0}\} \to g supp \underset{˙}{0} = (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0}$
29	28	eleq1d	$⊢ g = D \times \{\underset{˙}{0}\} \to (g supp \underset{˙}{0} \in A \leftrightarrow (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \in A)$
30	29	elrab	$⊢ D \times \{\underset{˙}{0}\} \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (D \times \{\underset{˙}{0}\} \in B \land (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \in A)$
31	27 30	bitrdi	$⊢ φ \to (D \times \{\underset{˙}{0}\} \in U \leftrightarrow (D \times \{\underset{˙}{0}\} \in B \land (D \times \{\underset{˙}{0}\}) supp \underset{˙}{0} \in A))$
32	13 26 31	mpbir2and	$⊢ φ \to D \times \{\underset{˙}{0}\} \in U$
33	32	ne0d	$⊢ φ \to U \neq \emptyset$
34		eqid	$⊢ +_{S} = +_{S}$
35	10	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to R \in Grp$
36	9	eleq2d	$⊢ φ \to (u \in U \leftrightarrow u \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
37		oveq1	$⊢ g = u \to g supp \underset{˙}{0} = u supp \underset{˙}{0}$
38	37	eleq1d	$⊢ g = u \to (g supp \underset{˙}{0} \in A \leftrightarrow u supp \underset{˙}{0} \in A)$
39	38	elrab	$⊢ u \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (u \in B \land u supp \underset{˙}{0} \in A)$
40	36 39	bitrdi	$⊢ φ \to (u \in U \leftrightarrow (u \in B \land u supp \underset{˙}{0} \in A))$
41	40	biimpa	$⊢ (φ \land u \in U) \to (u \in B \land u supp \underset{˙}{0} \in A)$
42	41	simpld	$⊢ (φ \land u \in U) \to u \in B$
43	42	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u \in B$
44	9	adantr	$⊢ (φ \land u \in U) \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
45	44	eleq2d	$⊢ (φ \land u \in U) \to (v \in U \leftrightarrow v \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
46		oveq1	$⊢ g = v \to g supp \underset{˙}{0} = v supp \underset{˙}{0}$
47	46	eleq1d	$⊢ g = v \to (g supp \underset{˙}{0} \in A \leftrightarrow v supp \underset{˙}{0} \in A)$
48	47	elrab	$⊢ v \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (v \in B \land v supp \underset{˙}{0} \in A)$
49	45 48	bitrdi	$⊢ (φ \land u \in U) \to (v \in U \leftrightarrow (v \in B \land v supp \underset{˙}{0} \in A))$
50	49	biimpa	$⊢ ((φ \land u \in U) \land v \in U) \to (v \in B \land v supp \underset{˙}{0} \in A)$
51	50	simpld	$⊢ ((φ \land u \in U) \land v \in U) \to v \in B$
52	1 2 34 35 43 51	psraddcl	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v \in B$
53		ovexd	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) supp \underset{˙}{0} \in V$
54		sseq2	$⊢ x = {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to (y \subseteq x \leftrightarrow y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))$
55	54	imbi1d	$⊢ x = {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to ((y \subseteq x \to y \in A) \leftrightarrow (y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to y \in A))$
56	55	albidv	$⊢ x = {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to (\forall y (y \subseteq x \to y \in A) \leftrightarrow \forall y (y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to y \in A))$
57	8	expr	$⊢ (φ \land x \in A) \to (y \subseteq x \to y \in A)$
58	57	alrimiv	$⊢ (φ \land x \in A) \to \forall y (y \subseteq x \to y \in A)$
59	58	ralrimiva	$⊢ φ \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
60	59	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
61	41	simprd	$⊢ (φ \land u \in U) \to u supp \underset{˙}{0} \in A$
62	61	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u supp \underset{˙}{0} \in A$
63	50	simprd	$⊢ ((φ \land u \in U) \land v \in U) \to v supp \underset{˙}{0} \in A$
64	7	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in A x \cup y \in A$
65	64	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to \forall x \in A \forall y \in A x \cup y \in A$
66		uneq1	$⊢ x = u supp \underset{˙}{0} \to x \cup y = {supp}_{\underset{˙}{0}} (u) \cup y$
67	66	eleq1d	$⊢ x = u supp \underset{˙}{0} \to (x \cup y \in A \leftrightarrow {supp}_{\underset{˙}{0}} (u) \cup y \in A)$
68		uneq2	$⊢ y = v supp \underset{˙}{0} \to {supp}_{\underset{˙}{0}} (u) \cup y = {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
69	68	eleq1d	$⊢ y = v supp \underset{˙}{0} \to ({supp}_{\underset{˙}{0}} (u) \cup y \in A \leftrightarrow {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \in A)$
70	67 69	rspc2va	$⊢ ((u supp \underset{˙}{0} \in A \land v supp \underset{˙}{0} \in A) \land \forall x \in A \forall y \in A x \cup y \in A) \to {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \in A$
71	62 63 65 70	syl21anc	$⊢ ((φ \land u \in U) \land v \in U) \to {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \in A$
72	56 60 71	rspcdva	$⊢ ((φ \land u \in U) \land v \in U) \to \forall y (y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to y \in A)$
73	1 14 4 2 52	psrelbas	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) : D ⟶ {Base}_{R}$
74		eqid	$⊢ +_{R} = +_{R}$
75	1 2 74 34 43 51	psradd	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v = u {+_{R}}_{f} v$
76	75	fveq1d	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) (k) = (u {+_{R}}_{f} v) (k)$
77	76	adantr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to (u +_{S} v) (k) = (u {+_{R}}_{f} v) (k)$
78		eldifi	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in D$
79	1 14 4 2 42	psrelbas	$⊢ (φ \land u \in U) \to u : D ⟶ {Base}_{R}$
80	79	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u : D ⟶ {Base}_{R}$
81	80	ffnd	$⊢ ((φ \land u \in U) \land v \in U) \to u Fn D$
82	1 14 4 2 51	psrelbas	$⊢ ((φ \land u \in U) \land v \in U) \to v : D ⟶ {Base}_{R}$
83	82	ffnd	$⊢ ((φ \land u \in U) \land v \in U) \to v Fn D$
84		ovex	$⊢ {ℕ_{0}}^{I} \in V$
85	4 84	rabex2	$⊢ D \in V$
86	85	a1i	$⊢ ((φ \land u \in U) \land v \in U) \to D \in V$
87		inidm	$⊢ D \cap D = D$
88		eqidd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to u (k) = u (k)$
89		eqidd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to v (k) = v (k)$
90	81 83 86 86 87 88 89	ofval	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to (u {+_{R}}_{f} v) (k) = u (k) +_{R} v (k)$
91	78 90	sylan2	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to (u {+_{R}}_{f} v) (k) = u (k) +_{R} v (k)$
92		ssun1	$⊢ u supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
93		sscon	$⊢ u supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (u)$
94	92 93	ax-mp	$⊢ D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (u)$
95	94	sseli	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in (D ∖ {supp}_{\underset{˙}{0}} (u))$
96		ssidd	$⊢ (φ \land u \in U) \to u supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
97	85	a1i	$⊢ (φ \land u \in U) \to D \in V$
98	19	a1i	$⊢ (φ \land u \in U) \to \underset{˙}{0} \in V$
99	79 96 97 98	suppssr	$⊢ ((φ \land u \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (u))) \to u (k) = \underset{˙}{0}$
100	99	adantlr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (u))) \to u (k) = \underset{˙}{0}$
101	95 100	sylan2	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to u (k) = \underset{˙}{0}$
102		ssun2	$⊢ v supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
103		sscon	$⊢ v supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (v)$
104	102 103	ax-mp	$⊢ D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (v)$
105	104	sseli	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in (D ∖ {supp}_{\underset{˙}{0}} (v))$
106		ssidd	$⊢ ((φ \land u \in U) \land v \in U) \to v supp \underset{˙}{0} \subseteq v supp \underset{˙}{0}$
107	19	a1i	$⊢ ((φ \land u \in U) \land v \in U) \to \underset{˙}{0} \in V$
108	82 106 86 107	suppssr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (v))) \to v (k) = \underset{˙}{0}$
109	105 108	sylan2	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to v (k) = \underset{˙}{0}$
110	101 109	oveq12d	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to u (k) +_{R} v (k) = \underset{˙}{0} +_{R} \underset{˙}{0}$
111	14 74 3	grplid	$⊢ (R \in Grp \land \underset{˙}{0} \in {Base}_{R}) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
112	35 15 111	syl2anc2	$⊢ ((φ \land u \in U) \land v \in U) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
113	112	adantr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
114	110 113	eqtrd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to u (k) +_{R} v (k) = \underset{˙}{0}$
115	77 91 114	3eqtrd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)))) \to (u +_{S} v) (k) = \underset{˙}{0}$
116	73 115	suppss	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
117		sseq1	$⊢ y = (u +_{S} v) supp \underset{˙}{0} \to (y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \leftrightarrow (u +_{S} v) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))$
118		eleq1	$⊢ y = (u +_{S} v) supp \underset{˙}{0} \to (y \in A \leftrightarrow (u +_{S} v) supp \underset{˙}{0} \in A)$
119	117 118	imbi12d	$⊢ y = (u +_{S} v) supp \underset{˙}{0} \to ((y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to y \in A) \leftrightarrow ((u +_{S} v) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to (u +_{S} v) supp \underset{˙}{0} \in A))$
120	119	spcgv	$⊢ (u +_{S} v) supp \underset{˙}{0} \in V \to (\forall y (y \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to y \in A) \to ((u +_{S} v) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \to (u +_{S} v) supp \underset{˙}{0} \in A))$
121	53 72 116 120	syl3c	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) supp \underset{˙}{0} \in A$
122	9	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
123	122	eleq2d	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v \in U \leftrightarrow u +_{S} v \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
124		oveq1	$⊢ g = u +_{S} v \to g supp \underset{˙}{0} = (u +_{S} v) supp \underset{˙}{0}$
125	124	eleq1d	$⊢ g = u +_{S} v \to (g supp \underset{˙}{0} \in A \leftrightarrow (u +_{S} v) supp \underset{˙}{0} \in A)$
126	125	elrab	$⊢ u +_{S} v \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (u +_{S} v \in B \land (u +_{S} v) supp \underset{˙}{0} \in A)$
127	123 126	bitrdi	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v \in U \leftrightarrow (u +_{S} v \in B \land (u +_{S} v) supp \underset{˙}{0} \in A))$
128	52 121 127	mpbir2and	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v \in U$
129	128	ralrimiva	$⊢ (φ \land u \in U) \to \forall v \in U u +_{S} v \in U$
130	1 5 10	psrgrp	$⊢ φ \to S \in Grp$
131		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
132	2 131	grpinvcl	$⊢ (S \in Grp \land u \in B) \to {inv}_{g} (S) (u) \in B$
133	130 42 132	syl2an2r	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) \in B$
134		ovexd	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in V$
135		sseq2	$⊢ x = u supp \underset{˙}{0} \to (y \subseteq x \leftrightarrow y \subseteq u supp \underset{˙}{0})$
136	135	imbi1d	$⊢ x = u supp \underset{˙}{0} \to ((y \subseteq x \to y \in A) \leftrightarrow (y \subseteq u supp \underset{˙}{0} \to y \in A))$
137	136	albidv	$⊢ x = u supp \underset{˙}{0} \to (\forall y (y \subseteq x \to y \in A) \leftrightarrow \forall y (y \subseteq u supp \underset{˙}{0} \to y \in A))$
138	59	adantr	$⊢ (φ \land u \in U) \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
139	137 138 61	rspcdva	$⊢ (φ \land u \in U) \to \forall y (y \subseteq u supp \underset{˙}{0} \to y \in A)$
140	5	adantr	$⊢ (φ \land u \in U) \to I \in W$
141	10	adantr	$⊢ (φ \land u \in U) \to R \in Grp$
142		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
143	1 140 141 4 142 2 131 42	psrneg	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) = {inv}_{g} (R) \circ u$
144	143	oveq1d	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} = ({inv}_{g} (R) \circ u) supp \underset{˙}{0}$
145	14 142	grpinvfn	$⊢ {inv}_{g} (R) Fn {Base}_{R}$
146	145	a1i	$⊢ (φ \land u \in U) \to {inv}_{g} (R) Fn {Base}_{R}$
147	3 142	grpinvid	$⊢ R \in Grp \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
148	141 147	syl	$⊢ (φ \land u \in U) \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
149	146 79 97 98 148	suppcoss	$⊢ (φ \land u \in U) \to ({inv}_{g} (R) \circ u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
150	144 149	eqsstrd	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
151		sseq1	$⊢ y = {inv}_{g} (S) (u) supp \underset{˙}{0} \to (y \subseteq u supp \underset{˙}{0} \leftrightarrow {inv}_{g} (S) (u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0})$
152		eleq1	$⊢ y = {inv}_{g} (S) (u) supp \underset{˙}{0} \to (y \in A \leftrightarrow {inv}_{g} (S) (u) supp \underset{˙}{0} \in A)$
153	151 152	imbi12d	$⊢ y = {inv}_{g} (S) (u) supp \underset{˙}{0} \to ((y \subseteq u supp \underset{˙}{0} \to y \in A) \leftrightarrow ({inv}_{g} (S) (u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0} \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in A))$
154	153	spcgv	$⊢ {inv}_{g} (S) (u) supp \underset{˙}{0} \in V \to (\forall y (y \subseteq u supp \underset{˙}{0} \to y \in A) \to ({inv}_{g} (S) (u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0} \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in A))$
155	134 139 150 154	syl3c	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in A$
156	44	eleq2d	$⊢ (φ \land u \in U) \to ({inv}_{g} (S) (u) \in U \leftrightarrow {inv}_{g} (S) (u) \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
157		oveq1	$⊢ g = {inv}_{g} (S) (u) \to g supp \underset{˙}{0} = {inv}_{g} (S) (u) supp \underset{˙}{0}$
158	157	eleq1d	$⊢ g = {inv}_{g} (S) (u) \to (g supp \underset{˙}{0} \in A \leftrightarrow {inv}_{g} (S) (u) supp \underset{˙}{0} \in A)$
159	158	elrab	$⊢ {inv}_{g} (S) (u) \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow ({inv}_{g} (S) (u) \in B \land {inv}_{g} (S) (u) supp \underset{˙}{0} \in A)$
160	156 159	bitrdi	$⊢ (φ \land u \in U) \to ({inv}_{g} (S) (u) \in U \leftrightarrow ({inv}_{g} (S) (u) \in B \land {inv}_{g} (S) (u) supp \underset{˙}{0} \in A))$
161	133 155 160	mpbir2and	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) \in U$
162	129 161	jca	$⊢ (φ \land u \in U) \to (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)$
163	162	ralrimiva	$⊢ φ \to \forall u \in U (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)$
164	2 34 131	issubg2	$⊢ S \in Grp \to (U \in SubGrp (S) \leftrightarrow (U \subseteq B \land U \neq \emptyset \land \forall u \in U (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)))$
165	130 164	syl	$⊢ φ \to (U \in SubGrp (S) \leftrightarrow (U \subseteq B \land U \neq \emptyset \land \forall u \in U (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)))$
166	12 33 163 165	mpbir3and	$⊢ φ \to U \in SubGrp (S)$

Metamath Proof Explorer

Theorem mplsubglem

Proof