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	grpmgmd	$⊢ φ \to R \in Mgm$
36	35	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to R \in Mgm$
37	9	eleq2d	$⊢ φ \to (u \in U \leftrightarrow u \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
38		oveq1	$⊢ g = u \to g supp \underset{˙}{0} = u supp \underset{˙}{0}$
39	38	eleq1d	$⊢ g = u \to (g supp \underset{˙}{0} \in A \leftrightarrow u supp \underset{˙}{0} \in A)$
40	39	elrab	$⊢ u \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (u \in B \land u supp \underset{˙}{0} \in A)$
41	37 40	bitrdi	$⊢ φ \to (u \in U \leftrightarrow (u \in B \land u supp \underset{˙}{0} \in A))$
42	41	biimpa	$⊢ (φ \land u \in U) \to (u \in B \land u supp \underset{˙}{0} \in A)$
43	42	simpld	$⊢ (φ \land u \in U) \to u \in B$
44	43	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u \in B$
45	9	adantr	$⊢ (φ \land u \in U) \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
46	45	eleq2d	$⊢ (φ \land u \in U) \to (v \in U \leftrightarrow v \in \{g \in B \| g supp \underset{˙}{0} \in A\})$
47		oveq1	$⊢ g = v \to g supp \underset{˙}{0} = v supp \underset{˙}{0}$
48	47	eleq1d	$⊢ g = v \to (g supp \underset{˙}{0} \in A \leftrightarrow v supp \underset{˙}{0} \in A)$
49	48	elrab	$⊢ v \in \{g \in B \| g supp \underset{˙}{0} \in A\} \leftrightarrow (v \in B \land v supp \underset{˙}{0} \in A)$
50	46 49	bitrdi	$⊢ (φ \land u \in U) \to (v \in U \leftrightarrow (v \in B \land v supp \underset{˙}{0} \in A))$
51	50	biimpa	$⊢ ((φ \land u \in U) \land v \in U) \to (v \in B \land v supp \underset{˙}{0} \in A)$
52	51	simpld	$⊢ ((φ \land u \in U) \land v \in U) \to v \in B$
53	1 2 34 36 44 52	psraddcl	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v \in B$
54		ovexd	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) supp \underset{˙}{0} \in V$
55		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))$
56	55	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))$
57	56	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))$
58	8	expr	$⊢ (φ \land x \in A) \to (y \subseteq x \to y \in A)$
59	58	alrimiv	$⊢ (φ \land x \in A) \to \forall y (y \subseteq x \to y \in A)$
60	59	ralrimiva	$⊢ φ \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
61	60	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
62	42	simprd	$⊢ (φ \land u \in U) \to u supp \underset{˙}{0} \in A$
63	62	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u supp \underset{˙}{0} \in A$
64	51	simprd	$⊢ ((φ \land u \in U) \land v \in U) \to v supp \underset{˙}{0} \in A$
65	7	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in A x \cup y \in A$
66	65	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to \forall x \in A \forall y \in A x \cup y \in A$
67		uneq1	$⊢ x = u supp \underset{˙}{0} \to x \cup y = {supp}_{\underset{˙}{0}} (u) \cup y$
68	67	eleq1d	$⊢ x = u supp \underset{˙}{0} \to (x \cup y \in A \leftrightarrow {supp}_{\underset{˙}{0}} (u) \cup y \in A)$
69		uneq2	$⊢ y = v supp \underset{˙}{0} \to {supp}_{\underset{˙}{0}} (u) \cup y = {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
70	69	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)$
71	68 70	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$
72	63 64 66 71	syl21anc	$⊢ ((φ \land u \in U) \land v \in U) \to {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v) \in A$
73	57 61 72	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)$
74	1 14 4 2 53	psrelbas	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) : D ⟶ {Base}_{R}$
75		eqid	$⊢ +_{R} = +_{R}$
76	1 2 75 34 44 52	psradd	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v = u {+_{R}}_{f} v$
77	76	fveq1d	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) (k) = (u {+_{R}}_{f} v) (k)$
78	77	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)$
79		eldifi	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in D$
80	1 14 4 2 43	psrelbas	$⊢ (φ \land u \in U) \to u : D ⟶ {Base}_{R}$
81	80	adantr	$⊢ ((φ \land u \in U) \land v \in U) \to u : D ⟶ {Base}_{R}$
82	81	ffnd	$⊢ ((φ \land u \in U) \land v \in U) \to u Fn D$
83	1 14 4 2 52	psrelbas	$⊢ ((φ \land u \in U) \land v \in U) \to v : D ⟶ {Base}_{R}$
84	83	ffnd	$⊢ ((φ \land u \in U) \land v \in U) \to v Fn D$
85		ovex	$⊢ {ℕ_{0}}^{I} \in V$
86	4 85	rabex2	$⊢ D \in V$
87	86	a1i	$⊢ ((φ \land u \in U) \land v \in U) \to D \in V$
88		inidm	$⊢ D \cap D = D$
89		eqidd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to u (k) = u (k)$
90		eqidd	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to v (k) = v (k)$
91	82 84 87 87 88 89 90	ofval	$⊢ (((φ \land u \in U) \land v \in U) \land k \in D) \to (u {+_{R}}_{f} v) (k) = u (k) +_{R} v (k)$
92	79 91	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)$
93		ssun1	$⊢ u supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
94		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)$
95	93 94	ax-mp	$⊢ D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (u)$
96	95	sseli	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in (D ∖ {supp}_{\underset{˙}{0}} (u))$
97		ssidd	$⊢ (φ \land u \in U) \to u supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
98	86	a1i	$⊢ (φ \land u \in U) \to D \in V$
99	19	a1i	$⊢ (φ \land u \in U) \to \underset{˙}{0} \in V$
100	80 97 98 99	suppssr	$⊢ ((φ \land u \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (u))) \to u (k) = \underset{˙}{0}$
101	100	adantlr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (u))) \to u (k) = \underset{˙}{0}$
102	96 101	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}$
103		ssun2	$⊢ v supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)$
104		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)$
105	103 104	ax-mp	$⊢ D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v)) \subseteq D ∖ {supp}_{\underset{˙}{0}} (v)$
106	105	sseli	$⊢ k \in (D ∖ ({supp}_{\underset{˙}{0}} (u) \cup {supp}_{\underset{˙}{0}} (v))) \to k \in (D ∖ {supp}_{\underset{˙}{0}} (v))$
107		ssidd	$⊢ ((φ \land u \in U) \land v \in U) \to v supp \underset{˙}{0} \subseteq v supp \underset{˙}{0}$
108	19	a1i	$⊢ ((φ \land u \in U) \land v \in U) \to \underset{˙}{0} \in V$
109	83 107 87 108	suppssr	$⊢ (((φ \land u \in U) \land v \in U) \land k \in (D ∖ {supp}_{\underset{˙}{0}} (v))) \to v (k) = \underset{˙}{0}$
110	106 109	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}$
111	102 110	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}$
112	10	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to R \in Grp$
113	14 75 3	grplid	$⊢ (R \in Grp \land \underset{˙}{0} \in {Base}_{R}) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
114	112 15 113	syl2anc2	$⊢ ((φ \land u \in U) \land v \in U) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
115	114	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}$
116	111 115	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}$
117	78 92 116	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}$
118	74 117	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)$
119		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))$
120		eleq1	$⊢ y = (u +_{S} v) supp \underset{˙}{0} \to (y \in A \leftrightarrow (u +_{S} v) supp \underset{˙}{0} \in A)$
121	119 120	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))$
122	121	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))$
123	54 73 118 122	syl3c	$⊢ ((φ \land u \in U) \land v \in U) \to (u +_{S} v) supp \underset{˙}{0} \in A$
124	9	ad2antrr	$⊢ ((φ \land u \in U) \land v \in U) \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
125	124	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\})$
126		oveq1	$⊢ g = u +_{S} v \to g supp \underset{˙}{0} = (u +_{S} v) supp \underset{˙}{0}$
127	126	eleq1d	$⊢ g = u +_{S} v \to (g supp \underset{˙}{0} \in A \leftrightarrow (u +_{S} v) supp \underset{˙}{0} \in A)$
128	127	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)$
129	125 128	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))$
130	53 123 129	mpbir2and	$⊢ ((φ \land u \in U) \land v \in U) \to u +_{S} v \in U$
131	130	ralrimiva	$⊢ (φ \land u \in U) \to \forall v \in U u +_{S} v \in U$
132	1 5 10	psrgrp	$⊢ φ \to S \in Grp$
133		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
134	2 133	grpinvcl	$⊢ (S \in Grp \land u \in B) \to {inv}_{g} (S) (u) \in B$
135	132 43 134	syl2an2r	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) \in B$
136		ovexd	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in V$
137		sseq2	$⊢ x = u supp \underset{˙}{0} \to (y \subseteq x \leftrightarrow y \subseteq u supp \underset{˙}{0})$
138	137	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))$
139	138	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))$
140	60	adantr	$⊢ (φ \land u \in U) \to \forall x \in A \forall y (y \subseteq x \to y \in A)$
141	139 140 62	rspcdva	$⊢ (φ \land u \in U) \to \forall y (y \subseteq u supp \underset{˙}{0} \to y \in A)$
142	5	adantr	$⊢ (φ \land u \in U) \to I \in W$
143	10	adantr	$⊢ (φ \land u \in U) \to R \in Grp$
144		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
145	1 142 143 4 144 2 133 43	psrneg	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) = {inv}_{g} (R) \circ u$
146	145	oveq1d	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} = ({inv}_{g} (R) \circ u) supp \underset{˙}{0}$
147	14 144	grpinvfn	$⊢ {inv}_{g} (R) Fn {Base}_{R}$
148	147	a1i	$⊢ (φ \land u \in U) \to {inv}_{g} (R) Fn {Base}_{R}$
149	3 144	grpinvid	$⊢ R \in Grp \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
150	143 149	syl	$⊢ (φ \land u \in U) \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
151	148 80 98 99 150	suppcoss	$⊢ (φ \land u \in U) \to ({inv}_{g} (R) \circ u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
152	146 151	eqsstrd	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \subseteq u supp \underset{˙}{0}$
153		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})$
154		eleq1	$⊢ y = {inv}_{g} (S) (u) supp \underset{˙}{0} \to (y \in A \leftrightarrow {inv}_{g} (S) (u) supp \underset{˙}{0} \in A)$
155	153 154	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))$
156	155	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))$
157	136 141 152 156	syl3c	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) supp \underset{˙}{0} \in A$
158	45	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\})$
159		oveq1	$⊢ g = {inv}_{g} (S) (u) \to g supp \underset{˙}{0} = {inv}_{g} (S) (u) supp \underset{˙}{0}$
160	159	eleq1d	$⊢ g = {inv}_{g} (S) (u) \to (g supp \underset{˙}{0} \in A \leftrightarrow {inv}_{g} (S) (u) supp \underset{˙}{0} \in A)$
161	160	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)$
162	158 161	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))$
163	135 157 162	mpbir2and	$⊢ (φ \land u \in U) \to {inv}_{g} (S) (u) \in U$
164	131 163	jca	$⊢ (φ \land u \in U) \to (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)$
165	164	ralrimiva	$⊢ φ \to \forall u \in U (\forall v \in U u +_{S} v \in U \land {inv}_{g} (S) (u) \in U)$
166	2 34 133	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)))$
167	132 166	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)))$
168	12 33 165 167	mpbir3and	$⊢ φ \to U \in SubGrp (S)$

Metamath Proof Explorer

Theorem mplsubglem

Proof