Theorem mplsubglem 19482

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

Hypotheses

Ref	Expression
mplsubglem.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
mplsubglem.b	⊢ 𝐵 = (Base‘𝑆)
mplsubglem.z	⊢ 0 = (0g‘𝑅)
mplsubglem.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
mplsubglem.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
mplsubglem.0	⊢ (𝜑 → ∅ ∈ 𝐴)
mplsubglem.a	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴)
mplsubglem.y	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴)
mplsubglem.u	⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})
mplsubglem.r	⊢ (𝜑 → 𝑅 ∈ Grp)

Assertion

Ref	Expression
mplsubglem	⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆))

Distinct variable groups:   𝑓,𝑔,𝑥,𝑦, 0   𝐴,𝑓,𝑔,𝑥,𝑦   𝐵,𝑓,𝑔   𝐷,𝑔   𝑓,𝐼   𝜑,𝑥,𝑦   𝑆,𝑓,𝑔,𝑦

Allowed substitution hints:   𝜑(𝑓,𝑔)   𝐵(𝑥,𝑦)   𝐷(𝑥,𝑦,𝑓)   𝑅(𝑥,𝑦,𝑓,𝑔)   𝑆(𝑥)   𝑈(𝑥,𝑦,𝑓,𝑔)   𝐼(𝑥,𝑦,𝑔)   𝑊(𝑥,𝑦,𝑓,𝑔)

Proof of Theorem mplsubglem

Dummy variables 𝑘 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplsubglem.u	. . 3 ⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})
2		ssrab2 3720	. . 3 ⊢ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ⊆ 𝐵
3	1, 2	syl6eqss 3688	. 2 ⊢ (𝜑 → 𝑈 ⊆ 𝐵)
4		mplsubglem.s	. . . . 5 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
5		mplsubglem.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
6		mplsubglem.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Grp)
7		mplsubglem.d	. . . . 5 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
8		mplsubglem.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
9		mplsubglem.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑆)
10	4, 5, 6, 7, 8, 9	psr0cl 19442	. . . 4 ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵)
11		eqid 2651	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
12	11, 8	grpidcl 17497	. . . . . . . 8 ⊢ (𝑅 ∈ Grp → 0 ∈ (Base‘𝑅))
13		fconst6g 6132	. . . . . . . 8 ⊢ ( 0 ∈ (Base‘𝑅) → (𝐷 × { 0 }):𝐷⟶(Base‘𝑅))
14	6, 12, 13	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐷 × { 0 }):𝐷⟶(Base‘𝑅))
15		eldifi 3765	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝐷 ∖ ∅) → 𝑢 ∈ 𝐷)
16		fvex 6239	. . . . . . . . . . 11 ⊢ (0g‘𝑅) ∈ V
17	8, 16	eqeltri 2726	. . . . . . . . . 10 ⊢ 0 ∈ V
18	17	fvconst2 6510	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐷 → ((𝐷 × { 0 })‘𝑢) = 0 )
19	15, 18	syl 17	. . . . . . . 8 ⊢ (𝑢 ∈ (𝐷 ∖ ∅) → ((𝐷 × { 0 })‘𝑢) = 0 )
20	19	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐷 ∖ ∅)) → ((𝐷 × { 0 })‘𝑢) = 0 )
21	14, 20	suppss 7370	. . . . . 6 ⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ⊆ ∅)
22		ss0 4007	. . . . . 6 ⊢ (((𝐷 × { 0 }) supp 0 ) ⊆ ∅ → ((𝐷 × { 0 }) supp 0 ) = ∅)
23	21, 22	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) = ∅)
24		mplsubglem.0	. . . . 5 ⊢ (𝜑 → ∅ ∈ 𝐴)
25	23, 24	eqeltrd 2730	. . . 4 ⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)
26	1	eleq2d 2716	. . . . 5 ⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ (𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
27		oveq1 6697	. . . . . . 7 ⊢ (𝑔 = (𝐷 × { 0 }) → (𝑔 supp 0 ) = ((𝐷 × { 0 }) supp 0 ))
28	27	eleq1d 2715	. . . . . 6 ⊢ (𝑔 = (𝐷 × { 0 }) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴))
29	28	elrab 3396	. . . . 5 ⊢ ((𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴))
30	26, 29	syl6bb 276	. . . 4 ⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)))
31	10, 25, 30	mpbir2and 977	. . 3 ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝑈)
32		ne0i 3954	. . 3 ⊢ ((𝐷 × { 0 }) ∈ 𝑈 → 𝑈 ≠ ∅)
33	31, 32	syl 17	. 2 ⊢ (𝜑 → 𝑈 ≠ ∅)
34		eqid 2651	. . . . . . 7 ⊢ (+g‘𝑆) = (+g‘𝑆)
35	6	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑅 ∈ Grp)
36	1	eleq2d 2716	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
37		oveq1 6697	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑢 → (𝑔 supp 0 ) = (𝑢 supp 0 ))
38	37	eleq1d 2715	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑢 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑢 supp 0 ) ∈ 𝐴))
39	38	elrab 3396	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴))
40	36, 39	syl6bb 276	. . . . . . . . . 10 ⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)))
41	40	biimpa 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴))
42	41	simpld 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐵)
43	42	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 ∈ 𝐵)
44	1	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})
45	44	eleq2d 2716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
46		oveq1 6697	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑣 → (𝑔 supp 0 ) = (𝑣 supp 0 ))
47	46	eleq1d 2715	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑣 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴))
48	47	elrab 3396	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))
49	45, 48	syl6bb 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)))
50	49	biimpa 500	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))
51	50	simpld 474	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 ∈ 𝐵)
52	4, 9, 34, 35, 43, 51	psraddcl 19431	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝐵)
53		ovexd 6720	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ V)
54	41	simprd 478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴)
55	54	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴)
56	50	simprd 478	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ∈ 𝐴)
57		mplsubglem.a	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴)
58	57	ralrimivva 3000	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴)
59	58	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴)
60		uneq1 3793	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢 supp 0 ) → (𝑥 ∪ 𝑦) = ((𝑢 supp 0 ) ∪ 𝑦))
61	60	eleq1d 2715	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑥 ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴))
62		uneq2 3794	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑣 supp 0 ) → ((𝑢 supp 0 ) ∪ 𝑦) = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))
63	62	eleq1d 2715	. . . . . . . . . 10 ⊢ (𝑦 = (𝑣 supp 0 ) → (((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴))
64	61, 63	rspc2va 3354	. . . . . . . . 9 ⊢ ((((𝑢 supp 0 ) ∈ 𝐴 ∧ (𝑣 supp 0 ) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴)
65	55, 56, 59, 64	syl21anc 1365	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴)
66		mplsubglem.y	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴)
67	66	expr 642	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴))
68	67	alrimiv 1895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴))
69	68	ralrimiva 2995	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴))
70	69	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴))
71		sseq2 3660	. . . . . . . . . . 11 ⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))))
72	71	imbi1d 330	. . . . . . . . . 10 ⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)))
73	72	albidv 1889	. . . . . . . . 9 ⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)))
74	73	rspcv 3336	. . . . . . . 8 ⊢ (((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)))
75	65, 70, 74	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))
76	4, 11, 7, 9, 52	psrelbas 19427	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣):𝐷⟶(Base‘𝑅))
77		eqid 2651	. . . . . . . . . . . 12 ⊢ (+g‘𝑅) = (+g‘𝑅)
78	4, 9, 77, 34, 43, 51	psradd 19430	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) = (𝑢 ∘𝑓 (+g‘𝑅)𝑣))
79	78	fveq1d 6231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓 (+g‘𝑅)𝑣)‘𝑘))
80	79	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓 (+g‘𝑅)𝑣)‘𝑘))
81		eldifi 3765	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ 𝐷)
82	4, 11, 7, 9, 42	psrelbas 19427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅))
83	82	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅))
84	83	ffnd 6084	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 Fn 𝐷)
85	4, 11, 7, 9, 51	psrelbas 19427	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣:𝐷⟶(Base‘𝑅))
86	85	ffnd 6084	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 Fn 𝐷)
87		ovex 6718	. . . . . . . . . . . . 13 ⊢ (ℕ0 ↑𝑚 𝐼) ∈ V
88	7, 87	rabex2 4847	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
89	88	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝐷 ∈ V)
90		inidm 3855	. . . . . . . . . . 11 ⊢ (𝐷 ∩ 𝐷) = 𝐷
91		eqidd 2652	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑢‘𝑘) = (𝑢‘𝑘))
92		eqidd 2652	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑣‘𝑘) = (𝑣‘𝑘))
93	84, 86, 89, 89, 90, 91, 92	ofval 6948	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → ((𝑢 ∘𝑓 (+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)))
94	81, 93	sylan2 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢 ∘𝑓 (+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)))
95		ssun1 3809	. . . . . . . . . . . . . 14 ⊢ (𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))
96		sscon 3777	. . . . . . . . . . . . . 14 ⊢ ((𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 )))
97	95, 96	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 ))
98	97	sseli 3632	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 )))
99		ssid 3657	. . . . . . . . . . . . . . 15 ⊢ (𝑢 supp 0 ) ⊆ (𝑢 supp 0 )
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ⊆ (𝑢 supp 0 ))
101	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐷 ∈ V)
102	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ∈ V)
103	82, 100, 101, 102	suppssr 7371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 )
104	103	adantlr 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 )
105	98, 104	sylan2 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑢‘𝑘) = 0 )
106		ssun2 3810	. . . . . . . . . . . . . 14 ⊢ (𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))
107		sscon 3777	. . . . . . . . . . . . . 14 ⊢ ((𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 )))
108	106, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 ))
109	108	sseli 3632	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 )))
110		ssid 3657	. . . . . . . . . . . . . 14 ⊢ (𝑣 supp 0 ) ⊆ (𝑣 supp 0 )
111	110	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ⊆ (𝑣 supp 0 ))
112	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 0 ∈ V)
113	85, 111, 89, 112	suppssr 7371	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑣‘𝑘) = 0 )
114	109, 113	sylan2 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑣‘𝑘) = 0 )
115	105, 114	oveq12d 6708	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = ( 0 (+g‘𝑅) 0 ))
116	11, 77, 8	grplid 17499	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Grp ∧ 0 ∈ (Base‘𝑅)) → ( 0 (+g‘𝑅) 0 ) = 0 )
117	12, 116	mpdan 703	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Grp → ( 0 (+g‘𝑅) 0 ) = 0 )
118	35, 117	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ( 0 (+g‘𝑅) 0 ) = 0 )
119	118	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ( 0 (+g‘𝑅) 0 ) = 0 )
120	115, 119	eqtrd 2685	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = 0 )
121	80, 94, 120	3eqtrd 2689	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = 0 )
122	76, 121	suppss 7370	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))
123		sseq1 3659	. . . . . . . . 9 ⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))))
124		eleq1 2718	. . . . . . . . 9 ⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))
125	123, 124	imbi12d 333	. . . . . . . 8 ⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → ((𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) ↔ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)))
126	125	spcgv 3324	. . . . . . 7 ⊢ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ V → (∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) → (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)))
127	53, 75, 122, 126	syl3c 66	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)
128	1	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})
129	128	eleq2d 2716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ (𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
130		oveq1 6697	. . . . . . . . 9 ⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → (𝑔 supp 0 ) = ((𝑢(+g‘𝑆)𝑣) supp 0 ))
131	130	eleq1d 2715	. . . . . . . 8 ⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))
132	131	elrab 3396	. . . . . . 7 ⊢ ((𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))
133	129, 132	syl6bb 276	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)))
134	52, 127, 133	mpbir2and 977	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝑈)
135	134	ralrimiva 2995	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈)
136	4, 5, 6	psrgrp 19446	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ Grp)
137		eqid 2651	. . . . . . 7 ⊢ (invg‘𝑆) = (invg‘𝑆)
138	9, 137	grpinvcl 17514	. . . . . 6 ⊢ ((𝑆 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((invg‘𝑆)‘𝑢) ∈ 𝐵)
139	136, 42, 138	syl2an2r 893	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝐵)
140		ovexd 6720	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ V)
141	69	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴))
142		sseq2 3660	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 supp 0 ) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑢 supp 0 )))
143	142	imbi1d 330	. . . . . . . . 9 ⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)))
144	143	albidv 1889	. . . . . . . 8 ⊢ (𝑥 = (𝑢 supp 0 ) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)))
145	144	rspcv 3336	. . . . . . 7 ⊢ ((𝑢 supp 0 ) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)))
146	54, 141, 145	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))
147	4, 11, 7, 9, 139	psrelbas 19427	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢):𝐷⟶(Base‘𝑅))
148	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐼 ∈ 𝑊)
149	6	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑅 ∈ Grp)
150		eqid 2651	. . . . . . . . . . 11 ⊢ (invg‘𝑅) = (invg‘𝑅)
151	4, 148, 149, 7, 150, 9, 137, 42	psrneg 19448	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢))
152	151	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → ((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢))
153	152	fveq1d 6231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (((invg‘𝑆)‘𝑢)‘𝑘) = (((invg‘𝑅) ∘ 𝑢)‘𝑘))
154		eldifi 3765	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 )) → 𝑘 ∈ 𝐷)
155		fvco3 6314	. . . . . . . . 9 ⊢ ((𝑢:𝐷⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐷) → (((invg‘𝑅) ∘ 𝑢)‘𝑘) = ((invg‘𝑅)‘(𝑢‘𝑘)))
156	82, 154, 155	syl2an 493	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (((invg‘𝑅) ∘ 𝑢)‘𝑘) = ((invg‘𝑅)‘(𝑢‘𝑘)))
157	103	fveq2d 6233	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → ((invg‘𝑅)‘(𝑢‘𝑘)) = ((invg‘𝑅)‘ 0 ))
158	8, 150	grpinvid 17523	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Grp → ((invg‘𝑅)‘ 0 ) = 0 )
159	149, 158	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑅)‘ 0 ) = 0 )
160	159	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → ((invg‘𝑅)‘ 0 ) = 0 )
161	157, 160	eqtrd 2685	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → ((invg‘𝑅)‘(𝑢‘𝑘)) = 0 )
162	153, 156, 161	3eqtrd 2689	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (((invg‘𝑆)‘𝑢)‘𝑘) = 0 )
163	147, 162	suppss 7370	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ))
164		sseq1 3659	. . . . . . . 8 ⊢ (𝑦 = (((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ⊆ (𝑢 supp 0 ) ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 )))
165		eleq1 2718	. . . . . . . 8 ⊢ (𝑦 = (((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))
166	164, 165	imbi12d 333	. . . . . . 7 ⊢ (𝑦 = (((invg‘𝑆)‘𝑢) supp 0 ) → ((𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) ↔ ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)))
167	166	spcgv 3324	. . . . . 6 ⊢ ((((invg‘𝑆)‘𝑢) supp 0 ) ∈ V → (∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) → ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)))
168	140, 146, 163, 167	syl3c 66	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)
169	44	eleq2d 2716	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ ((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
170		oveq1 6697	. . . . . . . 8 ⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → (𝑔 supp 0 ) = (((invg‘𝑆)‘𝑢) supp 0 ))
171	170	eleq1d 2715	. . . . . . 7 ⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))
172	171	elrab 3396	. . . . . 6 ⊢ (((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))
173	169, 172	syl6bb 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)))
174	139, 168, 173	mpbir2and 977	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝑈)
175	135, 174	jca 553	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈))
176	175	ralrimiva 2995	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈))
177	9, 34, 137	issubg2 17656	. . 3 ⊢ (𝑆 ∈ Grp → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈))))
178	136, 177	syl 17	. 2 ⊢ (𝜑 → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈))))
179	3, 33, 176, 178	mpbir3and 1264	1 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ⊆ wss 3607  ∅c0 3948  {csn 4210   × cxp 5141  ^◡ccnv 5142   “ cima 5146   ∘ ccom 5147  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ∘_𝑓 cof 6937   supp csupp 7340   ↑_𝑚 cmap 7899  Fincfn 7997  ℕcn 11058  ℕ₀cn0 11330  Basecbs 15904  +_gcplusg 15988  0_gc0g 16147  Grpcgrp 17469  inv_gcminusg 17470  SubGrpcsubg 17635   mPwSer cmps 19399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-sca 16004  df-vsca 16005  df-tset 16007  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472  df-minusg 17473  df-subg 17638  df-psr 19404

This theorem is referenced by:  mpllsslem  19483  mplsubg  19485