dprd2da

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dprd2d.1	$⊢ φ \to Rel A$
	dprd2d.2	$⊢ φ \to S : A ⟶ SubGrp (G)$
	dprd2d.3	$⊢ φ \to dom A \subseteq I$
	dprd2d.4	$⊢ (φ \land i \in I) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
	dprd2d.5	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
	dprd2d.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	dprd2da	$⊢ φ \to G dom DProd S$

Proof

Step	Hyp	Ref	Expression
1		dprd2d.1	$⊢ φ \to Rel A$
2		dprd2d.2	$⊢ φ \to S : A ⟶ SubGrp (G)$
3		dprd2d.3	$⊢ φ \to dom A \subseteq I$
4		dprd2d.4	$⊢ (φ \land i \in I) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
5		dprd2d.5	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
6		dprd2d.k	$⊢ K = mrCls (SubGrp (G))$
7		eqid	$⊢ Cntz (G) = Cntz (G)$
8		eqid	$⊢ 0_{G} = 0_{G}$
9		dprdgrp	$⊢ G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \to G \in Grp$
10	5 9	syl	$⊢ φ \to G \in Grp$
11		resiun2	$⊢ {A ↾}_{⋃_{i \in I} \{i\}} = ⋃_{i \in I} ({A ↾}_{\{i\}})$
12		iunid	$⊢ ⋃_{i \in I} \{i\} = I$
13	12	reseq2i	$⊢ {A ↾}_{⋃_{i \in I} \{i\}} = {A ↾}_{I}$
14	11 13	eqtr3i	$⊢ ⋃_{i \in I} ({A ↾}_{\{i\}}) = {A ↾}_{I}$
15		relssres	$⊢ (Rel A \land dom A \subseteq I) \to {A ↾}_{I} = A$
16	1 3 15	syl2anc	$⊢ φ \to {A ↾}_{I} = A$
17	14 16	syl5eq	$⊢ φ \to ⋃_{i \in I} ({A ↾}_{\{i\}}) = A$
18		ovex	$⊢ G DProd (j \in A [\{i\}] ⟼ i S j) \in V$
19		eqid	$⊢ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
20	18 19	dmmpti	$⊢ dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = I$
21		reldmdprd	$⊢ Rel dom DProd$
22	21	brrelex2i	$⊢ G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \in V$
23		dmexg	$⊢ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \in V \to dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \in V$
24	5 22 23	3syl	$⊢ φ \to dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \in V$
25	20 24	eqeltrrid	$⊢ φ \to I \in V$
26		ressn	$⊢ {A ↾}_{\{i\}} = \{i\} \times A [\{i\}]$
27		snex	$⊢ \{i\} \in V$
28		ovex	$⊢ i S j \in V$
29		eqid	$⊢ (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{i\}] ⟼ i S j)$
30	28 29	dmmpti	$⊢ dom (j \in A [\{i\}] ⟼ i S j) = A [\{i\}]$
31	21	brrelex2i	$⊢ G dom DProd (j \in A [\{i\}] ⟼ i S j) \to (j \in A [\{i\}] ⟼ i S j) \in V$
32		dmexg	$⊢ (j \in A [\{i\}] ⟼ i S j) \in V \to dom (j \in A [\{i\}] ⟼ i S j) \in V$
33	4 31 32	3syl	$⊢ (φ \land i \in I) \to dom (j \in A [\{i\}] ⟼ i S j) \in V$
34	30 33	eqeltrrid	$⊢ (φ \land i \in I) \to A [\{i\}] \in V$
35		xpexg	$⊢ (\{i\} \in V \land A [\{i\}] \in V) \to \{i\} \times A [\{i\}] \in V$
36	27 34 35	sylancr	$⊢ (φ \land i \in I) \to \{i\} \times A [\{i\}] \in V$
37	26 36	eqeltrid	$⊢ (φ \land i \in I) \to {A ↾}_{\{i\}} \in V$
38	37	ralrimiva	$⊢ φ \to \forall i \in I {A ↾}_{\{i\}} \in V$
39		iunexg	$⊢ (I \in V \land \forall i \in I {A ↾}_{\{i\}} \in V) \to ⋃_{i \in I} ({A ↾}_{\{i\}}) \in V$
40	25 38 39	syl2anc	$⊢ φ \to ⋃_{i \in I} ({A ↾}_{\{i\}}) \in V$
41	17 40	eqeltrrd	$⊢ φ \to A \in V$
42		sneq	$⊢ i = 1^{st} (x) \to \{i\} = \{1^{st} (x)\}$
43	42	imaeq2d	$⊢ i = 1^{st} (x) \to A [\{i\}] = A [\{1^{st} (x)\}]$
44		oveq1	$⊢ i = 1^{st} (x) \to i S j = 1^{st} (x) S j$
45	43 44	mpteq12dv	$⊢ i = 1^{st} (x) \to (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
46	45	breq2d	$⊢ i = 1^{st} (x) \to (G dom DProd (j \in A [\{i\}] ⟼ i S j) \leftrightarrow G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
47	4	ralrimiva	$⊢ φ \to \forall i \in I G dom DProd (j \in A [\{i\}] ⟼ i S j)$
48	47	adantr	$⊢ (φ \land x \in A) \to \forall i \in I G dom DProd (j \in A [\{i\}] ⟼ i S j)$
49	3	adantr	$⊢ (φ \land x \in A) \to dom A \subseteq I$
50		1stdm	$⊢ (Rel A \land x \in A) \to 1^{st} (x) \in dom A$
51	1 50	sylan	$⊢ (φ \land x \in A) \to 1^{st} (x) \in dom A$
52	49 51	sseldd	$⊢ (φ \land x \in A) \to 1^{st} (x) \in I$
53	46 48 52	rspcdva	$⊢ (φ \land x \in A) \to G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
54	53	3ad2antr1	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
55	54	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
56		ovex	$⊢ 1^{st} (x) S j \in V$
57		eqid	$⊢ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
58	56 57	dmmpti	$⊢ dom (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = A [\{1^{st} (x)\}]$
59	58	a1i	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to dom (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = A [\{1^{st} (x)\}]$
60		1st2nd	$⊢ (Rel A \land x \in A) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
61	1 60	sylan	$⊢ (φ \land x \in A) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
62		simpr	$⊢ (φ \land x \in A) \to x \in A$
63	61 62	eqeltrrd	$⊢ (φ \land x \in A) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in A$
64		df-br	$⊢ 1^{st} (x) A 2^{nd} (x) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in A$
65	63 64	sylibr	$⊢ (φ \land x \in A) \to 1^{st} (x) A 2^{nd} (x)$
66	1	adantr	$⊢ (φ \land x \in A) \to Rel A$
67		elrelimasn	$⊢ Rel A \to (2^{nd} (x) \in A [\{1^{st} (x)\}] \leftrightarrow 1^{st} (x) A 2^{nd} (x))$
68	66 67	syl	$⊢ (φ \land x \in A) \to (2^{nd} (x) \in A [\{1^{st} (x)\}] \leftrightarrow 1^{st} (x) A 2^{nd} (x))$
69	65 68	mpbird	$⊢ (φ \land x \in A) \to 2^{nd} (x) \in A [\{1^{st} (x)\}]$
70	69	3ad2antr1	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 2^{nd} (x) \in A [\{1^{st} (x)\}]$
71	70	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 2^{nd} (x) \in A [\{1^{st} (x)\}]$
72	1	adantr	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to Rel A$
73		simpr2	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to y \in A$
74		1st2nd	$⊢ (Rel A \land y \in A) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
75	72 73 74	syl2anc	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
76	75 73	eqeltrrd	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to ⟨1^{st} (y), 2^{nd} (y)⟩ \in A$
77		df-br	$⊢ 1^{st} (y) A 2^{nd} (y) \leftrightarrow ⟨1^{st} (y), 2^{nd} (y)⟩ \in A$
78	76 77	sylibr	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 1^{st} (y) A 2^{nd} (y)$
79		elrelimasn	$⊢ Rel A \to (2^{nd} (y) \in A [\{1^{st} (y)\}] \leftrightarrow 1^{st} (y) A 2^{nd} (y))$
80	72 79	syl	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (2^{nd} (y) \in A [\{1^{st} (y)\}] \leftrightarrow 1^{st} (y) A 2^{nd} (y))$
81	78 80	mpbird	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 2^{nd} (y) \in A [\{1^{st} (y)\}]$
82	81	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 2^{nd} (y) \in A [\{1^{st} (y)\}]$
83		simpr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 1^{st} (x) = 1^{st} (y)$
84	83	sneqd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to \{1^{st} (x)\} = \{1^{st} (y)\}$
85	84	imaeq2d	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to A [\{1^{st} (x)\}] = A [\{1^{st} (y)\}]$
86	82 85	eleqtrrd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 2^{nd} (y) \in A [\{1^{st} (x)\}]$
87		simplr3	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to x \neq y$
88		simpr1	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to x \in A$
89	72 88 60	syl2anc	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
90	89 75	eqeq12d	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (x = y \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩)$
91		fvex	$⊢ 1^{st} (x) \in V$
92		fvex	$⊢ 2^{nd} (x) \in V$
93	91 92	opth	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩ \leftrightarrow (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y))$
94	90 93	bitrdi	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (x = y \leftrightarrow (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) = 2^{nd} (y)))$
95	94	baibd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (x = y \leftrightarrow 2^{nd} (x) = 2^{nd} (y))$
96	95	necon3bid	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (x \neq y \leftrightarrow 2^{nd} (x) \neq 2^{nd} (y))$
97	87 96	mpbid	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 2^{nd} (x) \neq 2^{nd} (y)$
98	55 59 71 86 97 7	dprdcntz	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) \subseteq Cntz (G) ((j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (y)))$
99		df-ov	$⊢ 1^{st} (x) S 2^{nd} (x) = S (⟨1^{st} (x), 2^{nd} (x)⟩)$
100		oveq2	$⊢ j = 2^{nd} (x) \to 1^{st} (x) S j = 1^{st} (x) S 2^{nd} (x)$
101	100 57 56	fvmpt3i	$⊢ 2^{nd} (x) \in A [\{1^{st} (x)\}] \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = 1^{st} (x) S 2^{nd} (x)$
102	70 101	syl	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = 1^{st} (x) S 2^{nd} (x)$
103	89	fveq2d	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to S (x) = S (⟨1^{st} (x), 2^{nd} (x)⟩)$
104	99 102 103	3eqtr4a	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = S (x)$
105	104	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = S (x)$
106	83	oveq1d	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to 1^{st} (x) S j = 1^{st} (y) S j$
107	85 106	mpteq12dv	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
108	107	fveq1d	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (y)) = (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y))$
109		df-ov	$⊢ 1^{st} (y) S 2^{nd} (y) = S (⟨1^{st} (y), 2^{nd} (y)⟩)$
110		oveq2	$⊢ j = 2^{nd} (y) \to 1^{st} (y) S j = 1^{st} (y) S 2^{nd} (y)$
111		eqid	$⊢ (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) = (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
112		ovex	$⊢ 1^{st} (y) S j \in V$
113	110 111 112	fvmpt3i	$⊢ 2^{nd} (y) \in A [\{1^{st} (y)\}] \to (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y)) = 1^{st} (y) S 2^{nd} (y)$
114	81 113	syl	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y)) = 1^{st} (y) S 2^{nd} (y)$
115	75	fveq2d	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to S (y) = S (⟨1^{st} (y), 2^{nd} (y)⟩)$
116	109 114 115	3eqtr4a	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y)) = S (y)$
117	116	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y)) = S (y)$
118	108 117	eqtrd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (y)) = S (y)$
119	118	fveq2d	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to Cntz (G) ((j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (y))) = Cntz (G) (S (y))$
120	98 105 119	3sstr3d	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) = 1^{st} (y)) \to S (x) \subseteq Cntz (G) (S (y))$
121	1 2 3 4 5 6	dprd2dlem2	$⊢ (φ \land x \in A) \to S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
122	45	oveq2d	$⊢ i = 1^{st} (x) \to G DProd (j \in A [\{i\}] ⟼ i S j) = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
123	122 19 18	fvmpt3i	$⊢ 1^{st} (x) \in I \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
124	52 123	syl	$⊢ (φ \land x \in A) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
125	121 124	sseqtrrd	$⊢ (φ \land x \in A) \to S (x) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))$
126	125	3ad2antr1	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to S (x) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))$
127	126	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to S (x) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))$
128	5	ad2antrr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
129	20	a1i	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = I$
130	52	3ad2antr1	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 1^{st} (x) \in I$
131	130	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to 1^{st} (x) \in I$
132	3	adantr	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to dom A \subseteq I$
133		1stdm	$⊢ (Rel A \land y \in A) \to 1^{st} (y) \in dom A$
134	72 73 133	syl2anc	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 1^{st} (y) \in dom A$
135	132 134	sseldd	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to 1^{st} (y) \in I$
136	135	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to 1^{st} (y) \in I$
137		simpr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to 1^{st} (x) \neq 1^{st} (y)$
138	128 129 131 136 137 7	dprdcntz	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \subseteq Cntz (G) ((i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y)))$
139		sneq	$⊢ i = 1^{st} (y) \to \{i\} = \{1^{st} (y)\}$
140	139	imaeq2d	$⊢ i = 1^{st} (y) \to A [\{i\}] = A [\{1^{st} (y)\}]$
141		oveq1	$⊢ i = 1^{st} (y) \to i S j = 1^{st} (y) S j$
142	140 141	mpteq12dv	$⊢ i = 1^{st} (y) \to (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
143	142	oveq2d	$⊢ i = 1^{st} (y) \to G DProd (j \in A [\{i\}] ⟼ i S j) = G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
144	143 19 18	fvmpt3i	$⊢ 1^{st} (y) \in I \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y)) = G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
145	135 144	syl	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y)) = G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
146	145	fveq2d	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to Cntz (G) ((i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y))) = Cntz (G) (G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j))$
147		eqid	$⊢ {Base}_{G} = {Base}_{G}$
148	147	dprdssv	$⊢ G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) \subseteq {Base}_{G}$
149	142	breq2d	$⊢ i = 1^{st} (y) \to (G dom DProd (j \in A [\{i\}] ⟼ i S j) \leftrightarrow G dom DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j))$
150	47	adantr	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to \forall i \in I G dom DProd (j \in A [\{i\}] ⟼ i S j)$
151	149 150 135	rspcdva	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to G dom DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
152	112 111	dmmpti	$⊢ dom (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) = A [\{1^{st} (y)\}]$
153	152	a1i	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to dom (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) = A [\{1^{st} (y)\}]$
154	151 153 81	dprdub	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) (2^{nd} (y)) \subseteq G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
155	116 154	eqsstrrd	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to S (y) \subseteq G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)$
156	147 7	cntz2ss	$⊢ (G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j) \subseteq {Base}_{G} \land S (y) \subseteq G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)) \to Cntz (G) (G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)) \subseteq Cntz (G) (S (y))$
157	148 155 156	sylancr	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to Cntz (G) (G DProd (j \in A [\{1^{st} (y)\}] ⟼ 1^{st} (y) S j)) \subseteq Cntz (G) (S (y))$
158	146 157	eqsstrd	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to Cntz (G) ((i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y))) \subseteq Cntz (G) (S (y))$
159	158	adantr	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to Cntz (G) ((i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (y))) \subseteq Cntz (G) (S (y))$
160	138 159	sstrd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \subseteq Cntz (G) (S (y))$
161	127 160	sstrd	$⊢ ((φ \land (x \in A \land y \in A \land x \neq y)) \land 1^{st} (x) \neq 1^{st} (y)) \to S (x) \subseteq Cntz (G) (S (y))$
162	120 161	pm2.61dane	$⊢ (φ \land (x \in A \land y \in A \land x \neq y)) \to S (x) \subseteq Cntz (G) (S (y))$
163	10	adantr	$⊢ (φ \land x \in A) \to G \in Grp$
164	147	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
165		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
166	163 164 165	3syl	$⊢ (φ \land x \in A) \to SubGrp (G) \in Moore ({Base}_{G})$
167	16	adantr	$⊢ (φ \land x \in A) \to {A ↾}_{I} = A$
168		undif2	$⊢ \{1^{st} (x)\} \cup (I ∖ \{1^{st} (x)\}) = \{1^{st} (x)\} \cup I$
169	52	snssd	$⊢ (φ \land x \in A) \to \{1^{st} (x)\} \subseteq I$
170		ssequn1	$⊢ \{1^{st} (x)\} \subseteq I \leftrightarrow \{1^{st} (x)\} \cup I = I$
171	169 170	sylib	$⊢ (φ \land x \in A) \to \{1^{st} (x)\} \cup I = I$
172	168 171	syl5req	$⊢ (φ \land x \in A) \to I = \{1^{st} (x)\} \cup (I ∖ \{1^{st} (x)\})$
173	172	reseq2d	$⊢ (φ \land x \in A) \to {A ↾}_{I} = {A ↾}_{(\{1^{st} (x)\} \cup (I ∖ \{1^{st} (x)\}))}$
174	167 173	eqtr3d	$⊢ (φ \land x \in A) \to A = {A ↾}_{(\{1^{st} (x)\} \cup (I ∖ \{1^{st} (x)\}))}$
175		resundi	$⊢ {A ↾}_{(\{1^{st} (x)\} \cup (I ∖ \{1^{st} (x)\}))} = ({A ↾}_{\{1^{st} (x)\}}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
176	174 175	eqtrdi	$⊢ (φ \land x \in A) \to A = ({A ↾}_{\{1^{st} (x)\}}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
177	176	difeq1d	$⊢ (φ \land x \in A) \to A ∖ \{x\} = (({A ↾}_{\{1^{st} (x)\}}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})) ∖ \{x\}$
178		difundir	$⊢ (({A ↾}_{\{1^{st} (x)\}}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})) ∖ \{x\} = (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup (({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\})$
179	177 178	eqtrdi	$⊢ (φ \land x \in A) \to A ∖ \{x\} = (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup (({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\})$
180		neirr	$⊢ \neg 1^{st} (x) \neq 1^{st} (x)$
181	61	eleq1d	$⊢ (φ \land x \in A) \to (x \in ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{(I ∖ \{1^{st} (x)\})}))$
182		df-br	$⊢ 1^{st} (x) ({A ↾}_{(I ∖ \{1^{st} (x)\})}) 2^{nd} (x) \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
183	92	brresi	$⊢ 1^{st} (x) ({A ↾}_{(I ∖ \{1^{st} (x)\})}) 2^{nd} (x) \leftrightarrow (1^{st} (x) \in (I ∖ \{1^{st} (x)\}) \land 1^{st} (x) A 2^{nd} (x))$
184	183	simplbi	$⊢ 1^{st} (x) ({A ↾}_{(I ∖ \{1^{st} (x)\})}) 2^{nd} (x) \to 1^{st} (x) \in (I ∖ \{1^{st} (x)\})$
185		eldifsni	$⊢ 1^{st} (x) \in (I ∖ \{1^{st} (x)\}) \to 1^{st} (x) \neq 1^{st} (x)$
186	184 185	syl	$⊢ 1^{st} (x) ({A ↾}_{(I ∖ \{1^{st} (x)\})}) 2^{nd} (x) \to 1^{st} (x) \neq 1^{st} (x)$
187	182 186	sylbir	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \to 1^{st} (x) \neq 1^{st} (x)$
188	181 187	syl6bi	$⊢ (φ \land x \in A) \to (x \in ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \to 1^{st} (x) \neq 1^{st} (x))$
189	180 188	mtoi	$⊢ (φ \land x \in A) \to \neg x \in ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
190		disjsn	$⊢ ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \cap \{x\} = \emptyset \leftrightarrow \neg x \in ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
191	189 190	sylibr	$⊢ (φ \land x \in A) \to ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \cap \{x\} = \emptyset$
192		disj3	$⊢ ({A ↾}_{(I ∖ \{1^{st} (x)\})}) \cap \{x\} = \emptyset \leftrightarrow {A ↾}_{(I ∖ \{1^{st} (x)\})} = ({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\}$
193	191 192	sylib	$⊢ (φ \land x \in A) \to {A ↾}_{(I ∖ \{1^{st} (x)\})} = ({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\}$
194	193	eqcomd	$⊢ (φ \land x \in A) \to ({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\} = {A ↾}_{(I ∖ \{1^{st} (x)\})}$
195	194	uneq2d	$⊢ (φ \land x \in A) \to (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup (({A ↾}_{(I ∖ \{1^{st} (x)\})}) ∖ \{x\}) = (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
196	179 195	eqtrd	$⊢ (φ \land x \in A) \to A ∖ \{x\} = (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})$
197	196	imaeq2d	$⊢ (φ \land x \in A) \to S [A ∖ \{x\}] = S [(({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})]$
198		imaundi	$⊢ S [(({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \cup ({A ↾}_{(I ∖ \{1^{st} (x)\})})] = S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]$
199	197 198	eqtrdi	$⊢ (φ \land x \in A) \to S [A ∖ \{x\}] = S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]$
200	199	unieqd	$⊢ (φ \land x \in A) \to ⋃ S [A ∖ \{x\}] = ⋃ (S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
201		uniun	$⊢ ⋃ (S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]$
202	200 201	eqtrdi	$⊢ (φ \land x \in A) \to ⋃ S [A ∖ \{x\}] = ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]$
203		imassrn	$⊢ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq ran S$
204	2	frnd	$⊢ φ \to ran S \subseteq SubGrp (G)$
205	204	adantr	$⊢ (φ \land x \in A) \to ran S \subseteq SubGrp (G)$
206		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
207	166 206	syl	$⊢ (φ \land x \in A) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
208	205 207	sstrd	$⊢ (φ \land x \in A) \to ran S \subseteq 𝒫 {Base}_{G}$
209	203 208	sstrid	$⊢ (φ \land x \in A) \to S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq 𝒫 {Base}_{G}$
210		sspwuni	$⊢ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq {Base}_{G}$
211	209 210	sylib	$⊢ (φ \land x \in A) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq {Base}_{G}$
212	166 6 211	mrcssidd	$⊢ (φ \land x \in A) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}])$
213		imassrn	$⊢ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq ran S$
214	213 208	sstrid	$⊢ (φ \land x \in A) \to S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq 𝒫 {Base}_{G}$
215		sspwuni	$⊢ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq {Base}_{G}$
216	214 215	sylib	$⊢ (φ \land x \in A) \to ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq {Base}_{G}$
217	166 6 216	mrcssidd	$⊢ (φ \land x \in A) \to ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
218		unss12	$⊢ (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \land ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cup K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
219	212 217 218	syl2anc	$⊢ (φ \land x \in A) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \cup ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cup K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
220	202 219	eqsstrd	$⊢ (φ \land x \in A) \to ⋃ S [A ∖ \{x\}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cup K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
221	6	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq {Base}_{G}) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G)$
222	166 211 221	syl2anc	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G)$
223	6	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}] \subseteq {Base}_{G}) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)$
224	166 216 223	syl2anc	$⊢ (φ \land x \in A) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)$
225		eqid	$⊢ LSSum (G) = LSSum (G)$
226	225	lsmunss	$⊢ (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G) \land K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cup K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
227	222 224 226	syl2anc	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cup K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
228	220 227	sstrd	$⊢ (φ \land x \in A) \to ⋃ S [A ∖ \{x\}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
229		difss	$⊢ ({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\} \subseteq {A ↾}_{\{1^{st} (x)\}}$
230		ressn	$⊢ {A ↾}_{\{1^{st} (x)\}} = \{1^{st} (x)\} \times A [\{1^{st} (x)\}]$
231	229 230	sseqtri	$⊢ ({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\} \subseteq \{1^{st} (x)\} \times A [\{1^{st} (x)\}]$
232		imass2	$⊢ ({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\} \subseteq \{1^{st} (x)\} \times A [\{1^{st} (x)\}] \to S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq S [\{1^{st} (x)\} \times A [\{1^{st} (x)\}]]$
233	231 232	ax-mp	$⊢ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq S [\{1^{st} (x)\} \times A [\{1^{st} (x)\}]]$
234		ovex	$⊢ 1^{st} (x) S i \in V$
235		oveq2	$⊢ j = i \to 1^{st} (x) S j = 1^{st} (x) S i$
236	57 235	elrnmpt1s	$⊢ (i \in A [\{1^{st} (x)\}] \land 1^{st} (x) S i \in V) \to 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
237	234 236	mpan2	$⊢ i \in A [\{1^{st} (x)\}] \to 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
238	237	rgen	$⊢ \forall i \in A [\{1^{st} (x)\}] 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
239	238	a1i	$⊢ (φ \land x \in A) \to \forall i \in A [\{1^{st} (x)\}] 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
240		oveq1	$⊢ y = 1^{st} (x) \to y S i = 1^{st} (x) S i$
241	240	eleq1d	$⊢ y = 1^{st} (x) \to (y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \leftrightarrow 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
242	241	ralbidv	$⊢ y = 1^{st} (x) \to (\forall i \in A [\{1^{st} (x)\}] y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \leftrightarrow \forall i \in A [\{1^{st} (x)\}] 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
243	91 242	ralsn	$⊢ \forall y \in \{1^{st} (x)\} \forall i \in A [\{1^{st} (x)\}] y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \leftrightarrow \forall i \in A [\{1^{st} (x)\}] 1^{st} (x) S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
244	239 243	sylibr	$⊢ (φ \land x \in A) \to \forall y \in \{1^{st} (x)\} \forall i \in A [\{1^{st} (x)\}] y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
245	2	adantr	$⊢ (φ \land x \in A) \to S : A ⟶ SubGrp (G)$
246	245	ffund	$⊢ (φ \land x \in A) \to Fun S$
247		resss	$⊢ {A ↾}_{\{1^{st} (x)\}} \subseteq A$
248	230 247	eqsstrri	$⊢ \{1^{st} (x)\} \times A [\{1^{st} (x)\}] \subseteq A$
249	245	fdmd	$⊢ (φ \land x \in A) \to dom S = A$
250	248 249	sseqtrrid	$⊢ (φ \land x \in A) \to \{1^{st} (x)\} \times A [\{1^{st} (x)\}] \subseteq dom S$
251		funimassov	$⊢ (Fun S \land \{1^{st} (x)\} \times A [\{1^{st} (x)\}] \subseteq dom S) \to (S [\{1^{st} (x)\} \times A [\{1^{st} (x)\}]] \subseteq ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \leftrightarrow \forall y \in \{1^{st} (x)\} \forall i \in A [\{1^{st} (x)\}] y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
252	246 250 251	syl2anc	$⊢ (φ \land x \in A) \to (S [\{1^{st} (x)\} \times A [\{1^{st} (x)\}]] \subseteq ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \leftrightarrow \forall y \in \{1^{st} (x)\} \forall i \in A [\{1^{st} (x)\}] y S i \in ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
253	244 252	mpbird	$⊢ (φ \land x \in A) \to S [\{1^{st} (x)\} \times A [\{1^{st} (x)\}]] \subseteq ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
254	233 253	sstrid	$⊢ (φ \land x \in A) \to S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
255	254	unissd	$⊢ (φ \land x \in A) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq ⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
256		df-ov	$⊢ 1^{st} (x) S j = S (⟨1^{st} (x), j⟩)$
257	2	ad2antrr	$⊢ ((φ \land x \in A) \land j \in A [\{1^{st} (x)\}]) \to S : A ⟶ SubGrp (G)$
258		elrelimasn	$⊢ Rel A \to (j \in A [\{1^{st} (x)\}] \leftrightarrow 1^{st} (x) A j)$
259	66 258	syl	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] \leftrightarrow 1^{st} (x) A j)$
260	259	biimpa	$⊢ ((φ \land x \in A) \land j \in A [\{1^{st} (x)\}]) \to 1^{st} (x) A j$
261		df-br	$⊢ 1^{st} (x) A j \leftrightarrow ⟨1^{st} (x), j⟩ \in A$
262	260 261	sylib	$⊢ ((φ \land x \in A) \land j \in A [\{1^{st} (x)\}]) \to ⟨1^{st} (x), j⟩ \in A$
263	257 262	ffvelrnd	$⊢ ((φ \land x \in A) \land j \in A [\{1^{st} (x)\}]) \to S (⟨1^{st} (x), j⟩) \in SubGrp (G)$
264	256 263	eqeltrid	$⊢ ((φ \land x \in A) \land j \in A [\{1^{st} (x)\}]) \to 1^{st} (x) S j \in SubGrp (G)$
265	264	fmpttd	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) : A [\{1^{st} (x)\}] ⟶ SubGrp (G)$
266	265	frnd	$⊢ (φ \land x \in A) \to ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq SubGrp (G)$
267	266 207	sstrd	$⊢ (φ \land x \in A) \to ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq 𝒫 {Base}_{G}$
268		sspwuni	$⊢ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq {Base}_{G}$
269	267 268	sylib	$⊢ (φ \land x \in A) \to ⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq {Base}_{G}$
270	166 6 255 269	mrcssd	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq K (⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
271	6	dprdspan	$⊢ G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = K (⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
272	53 271	syl	$⊢ (φ \land x \in A) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = K (⋃ ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
273	270 272	sseqtrrd	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
274	18 19	fnmpti	$⊢ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) Fn I$
275		fnressn	$⊢ ((i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) Fn I \land 1^{st} (x) \in I) \to {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}} = \{⟨1^{st} (x), (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))⟩\}$
276	274 52 275	sylancr	$⊢ (φ \land x \in A) \to {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}} = \{⟨1^{st} (x), (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))⟩\}$
277	124	opeq2d	$⊢ (φ \land x \in A) \to ⟨1^{st} (x), (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))⟩ = ⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩$
278	277	sneqd	$⊢ (φ \land x \in A) \to \{⟨1^{st} (x), (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))⟩\} = \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\}$
279	276 278	eqtrd	$⊢ (φ \land x \in A) \to {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}} = \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\}$
280	279	oveq2d	$⊢ (φ \land x \in A) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}}) = G DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\}$
281		dprdsubg	$⊢ G dom DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in SubGrp (G)$
282	53 281	syl	$⊢ (φ \land x \in A) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in SubGrp (G)$
283		dprdsn	$⊢ (1^{st} (x) \in I \land G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in SubGrp (G)) \to (G dom DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\} \land G DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\} = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
284	52 282 283	syl2anc	$⊢ (φ \land x \in A) \to (G dom DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\} \land G DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\} = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
285	284	simprd	$⊢ (φ \land x \in A) \to G DProd \{⟨1^{st} (x), G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)⟩\} = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
286	280 285	eqtrd	$⊢ (φ \land x \in A) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}}) = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
287	5	adantr	$⊢ (φ \land x \in A) \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
288	20	a1i	$⊢ (φ \land x \in A) \to dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = I$
289		difss	$⊢ I ∖ \{1^{st} (x)\} \subseteq I$
290	289	a1i	$⊢ (φ \land x \in A) \to I ∖ \{1^{st} (x)\} \subseteq I$
291		disjdif	$⊢ \{1^{st} (x)\} \cap (I ∖ \{1^{st} (x)\}) = \emptyset$
292	291	a1i	$⊢ (φ \land x \in A) \to \{1^{st} (x)\} \cap (I ∖ \{1^{st} (x)\}) = \emptyset$
293	287 288 169 290 292 7	dprdcntz2	$⊢ (φ \land x \in A) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{\{1^{st} (x)\}}) \subseteq Cntz (G) (G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
294	286 293	eqsstrrd	$⊢ (φ \land x \in A) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq Cntz (G) (G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
295	4	adantlr	$⊢ ((φ \land x \in A) \land i \in I) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
296	66 245 49 295 287 6 290	dprd2dlem1	$⊢ (φ \land x \in A) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = G DProd (i \in (I ∖ \{1^{st} (x)\}) ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
297		resmpt	$⊢ I ∖ \{1^{st} (x)\} \subseteq I \to {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})} = (i \in (I ∖ \{1^{st} (x)\}) ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
298	289 297	ax-mp	$⊢ {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})} = (i \in (I ∖ \{1^{st} (x)\}) ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
299	298	oveq2i	$⊢ G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) = G DProd (i \in (I ∖ \{1^{st} (x)\}) ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
300	296 299	eqtr4di	$⊢ (φ \land x \in A) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})})$
301	300	fveq2d	$⊢ (φ \land x \in A) \to Cntz (G) (K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])) = Cntz (G) (G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
302	294 301	sseqtrrd	$⊢ (φ \land x \in A) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq Cntz (G) (K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))$
303	273 302	sstrd	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq Cntz (G) (K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))$
304	225 7	lsmsubg	$⊢ (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G) \land K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G) \land K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq Cntz (G) (K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)$
305	222 224 303 304	syl3anc	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)$
306	6	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [A ∖ \{x\}] \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \land K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G)) \to K (⋃ S [A ∖ \{x\}]) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
307	166 228 305 306	syl3anc	$⊢ (φ \land x \in A) \to K (⋃ S [A ∖ \{x\}]) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
308		sslin	$⊢ K (⋃ S [A ∖ \{x\}]) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \to S (x) \cap K (⋃ S [A ∖ \{x\}]) \subseteq S (x) \cap (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))$
309	307 308	syl	$⊢ (φ \land x \in A) \to S (x) \cap K (⋃ S [A ∖ \{x\}]) \subseteq S (x) \cap (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))$
310	2	ffvelrnda	$⊢ (φ \land x \in A) \to S (x) \in SubGrp (G)$
311	225	lsmlub	$⊢ (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G) \land S (x) \in SubGrp (G) \land G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in SubGrp (G)) \to ((K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \land S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)) \leftrightarrow K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
312	222 310 282 311	syl3anc	$⊢ (φ \land x \in A) \to ((K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \land S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)) \leftrightarrow K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j))$
313	273 121 312	mpbi2and	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
314	313 124	sseqtrrd	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x))$
315	287 288 290	dprdres	$⊢ (φ \land x \in A) \to (G dom DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) \land G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) \subseteq G DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
316	315	simpld	$⊢ (φ \land x \in A) \to G dom DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})})$
317	6	dprdspan	$⊢ G dom DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) = K (⋃ ran ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
318	316 317	syl	$⊢ (φ \land x \in A) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) = K (⋃ ran ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
319		df-ima	$⊢ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}] = ran ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})})$
320	319	unieqi	$⊢ ⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}] = ⋃ ran ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})})$
321	320	fveq2i	$⊢ K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}]) = K (⋃ ran ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}))$
322	318 321	eqtr4di	$⊢ (φ \land x \in A) \to G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{(I ∖ \{1^{st} (x)\})}) = K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
323	300 322	eqtrd	$⊢ (φ \land x \in A) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
324		eqimss	$⊢ K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}]) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
325	323 324	syl	$⊢ (φ \land x \in A) \to K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
326		ss2in	$⊢ (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \land K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])) \to (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \cap K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
327	314 325 326	syl2anc	$⊢ (φ \land x \in A) \to (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \cap K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}])$
328	287 288 52 8 6	dprddisj	$⊢ (φ \land x \in A) \to (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) (1^{st} (x)) \cap K (⋃ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) [I ∖ \{1^{st} (x)\}]) = \{0_{G}\}$
329	327 328	sseqtrd	$⊢ (φ \land x \in A) \to (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \subseteq \{0_{G}\}$
330	225	lsmub2	$⊢ (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G) \land S (x) \in SubGrp (G)) \to S (x) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)$
331	222 310 330	syl2anc	$⊢ (φ \land x \in A) \to S (x) \subseteq K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)$
332	8	subg0cl	$⊢ S (x) \in SubGrp (G) \to 0_{G} \in S (x)$
333	310 332	syl	$⊢ (φ \land x \in A) \to 0_{G} \in S (x)$
334	331 333	sseldd	$⊢ (φ \land x \in A) \to 0_{G} \in (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x))$
335	8	subg0cl	$⊢ K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) \in SubGrp (G) \to 0_{G} \in K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
336	224 335	syl	$⊢ (φ \land x \in A) \to 0_{G} \in K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
337	334 336	elind	$⊢ (φ \land x \in A) \to 0_{G} \in ((K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]))$
338	337	snssd	$⊢ (φ \land x \in A) \to \{0_{G}\} \subseteq (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])$
339	329 338	eqssd	$⊢ (φ \land x \in A) \to (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) S (x)) \cap K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}]) = \{0_{G}\}$
340		incom	$⊢ K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cap S (x) = S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}])$
341	69 101	syl	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = 1^{st} (x) S 2^{nd} (x)$
342	61	fveq2d	$⊢ (φ \land x \in A) \to S (x) = S (⟨1^{st} (x), 2^{nd} (x)⟩)$
343	99 341 342	3eqtr4a	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = S (x)$
344		eqimss2	$⊢ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) = S (x) \to S (x) \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x))$
345	343 344	syl	$⊢ (φ \land x \in A) \to S (x) \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x))$
346		eldifsn	$⊢ y \in (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \leftrightarrow (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)$
347	1	ad2antrr	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to Rel A$
348		simprl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to y \in ({A ↾}_{\{1^{st} (x)\}})$
349	247 348	sseldi	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to y \in A$
350	347 349 74	syl2anc	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
351	350	fveq2d	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to S (y) = S (⟨1^{st} (y), 2^{nd} (y)⟩)$
352	351 109	eqtr4di	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to S (y) = 1^{st} (y) S 2^{nd} (y)$
353	350 348	eqeltrrd	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to ⟨1^{st} (y), 2^{nd} (y)⟩ \in ({A ↾}_{\{1^{st} (x)\}})$
354		fvex	$⊢ 2^{nd} (y) \in V$
355	354	opelresi	$⊢ ⟨1^{st} (y), 2^{nd} (y)⟩ \in ({A ↾}_{\{1^{st} (x)\}}) \leftrightarrow (1^{st} (y) \in \{1^{st} (x)\} \land ⟨1^{st} (y), 2^{nd} (y)⟩ \in A)$
356	355	simplbi	$⊢ ⟨1^{st} (y), 2^{nd} (y)⟩ \in ({A ↾}_{\{1^{st} (x)\}}) \to 1^{st} (y) \in \{1^{st} (x)\}$
357	353 356	syl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 1^{st} (y) \in \{1^{st} (x)\}$
358		elsni	$⊢ 1^{st} (y) \in \{1^{st} (x)\} \to 1^{st} (y) = 1^{st} (x)$
359	357 358	syl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 1^{st} (y) = 1^{st} (x)$
360	359	oveq1d	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 1^{st} (y) S 2^{nd} (y) = 1^{st} (x) S 2^{nd} (y)$
361	352 360	eqtrd	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to S (y) = 1^{st} (x) S 2^{nd} (y)$
362	348 230	eleqtrdi	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to y \in (\{1^{st} (x)\} \times A [\{1^{st} (x)\}])$
363		xp2nd	$⊢ y \in (\{1^{st} (x)\} \times A [\{1^{st} (x)\}]) \to 2^{nd} (y) \in A [\{1^{st} (x)\}]$
364	362 363	syl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 2^{nd} (y) \in A [\{1^{st} (x)\}]$
365		simprr	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to y \neq x$
366	61	adantr	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
367	350 366	eqeq12d	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to (y = x \leftrightarrow ⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨1^{st} (x), 2^{nd} (x)⟩)$
368		fvex	$⊢ 1^{st} (y) \in V$
369	368 354	opth	$⊢ ⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨1^{st} (x), 2^{nd} (x)⟩ \leftrightarrow (1^{st} (y) = 1^{st} (x) \land 2^{nd} (y) = 2^{nd} (x))$
370	369	baib	$⊢ 1^{st} (y) = 1^{st} (x) \to (⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨1^{st} (x), 2^{nd} (x)⟩ \leftrightarrow 2^{nd} (y) = 2^{nd} (x))$
371	359 370	syl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to (⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨1^{st} (x), 2^{nd} (x)⟩ \leftrightarrow 2^{nd} (y) = 2^{nd} (x))$
372	367 371	bitrd	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to (y = x \leftrightarrow 2^{nd} (y) = 2^{nd} (x))$
373	372	necon3bid	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to (y \neq x \leftrightarrow 2^{nd} (y) \neq 2^{nd} (x))$
374	365 373	mpbid	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 2^{nd} (y) \neq 2^{nd} (x)$
375		eldifsn	$⊢ 2^{nd} (y) \in (A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}) \leftrightarrow (2^{nd} (y) \in A [\{1^{st} (x)\}] \land 2^{nd} (y) \neq 2^{nd} (x))$
376	364 374 375	sylanbrc	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 2^{nd} (y) \in (A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})$
377		ovex	$⊢ 1^{st} (x) S 2^{nd} (y) \in V$
378		difss	$⊢ A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\} \subseteq A [\{1^{st} (x)\}]$
379		resmpt	$⊢ A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\} \subseteq A [\{1^{st} (x)\}] \to {(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})} = (j \in (A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}) ⟼ 1^{st} (x) S j)$
380	378 379	ax-mp	$⊢ {(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})} = (j \in (A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}) ⟼ 1^{st} (x) S j)$
381		oveq2	$⊢ j = 2^{nd} (y) \to 1^{st} (x) S j = 1^{st} (x) S 2^{nd} (y)$
382	380 381	elrnmpt1s	$⊢ (2^{nd} (y) \in (A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}) \land 1^{st} (x) S 2^{nd} (y) \in V) \to 1^{st} (x) S 2^{nd} (y) \in ran ({(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})})$
383	376 377 382	sylancl	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to 1^{st} (x) S 2^{nd} (y) \in ran ({(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})})$
384	361 383	eqeltrd	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to S (y) \in ran ({(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})})$
385		df-ima	$⊢ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] = ran ({(j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) ↾}_{(A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\})})$
386	384 385	eleqtrrdi	$⊢ ((φ \land x \in A) \land (y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x)) \to S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}]$
387	386	ex	$⊢ (φ \land x \in A) \to ((y \in ({A ↾}_{\{1^{st} (x)\}}) \land y \neq x) \to S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
388	346 387	syl5bi	$⊢ (φ \land x \in A) \to (y \in (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) \to S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
389	388	ralrimiv	$⊢ (φ \land x \in A) \to \forall y \in (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}]$
390	231 250	sstrid	$⊢ (φ \land x \in A) \to ({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\} \subseteq dom S$
391		funimass4	$⊢ (Fun S \land ({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\} \subseteq dom S) \to (S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \leftrightarrow \forall y \in (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
392	246 390 391	syl2anc	$⊢ (φ \land x \in A) \to (S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \leftrightarrow \forall y \in (({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}) S (y) \in (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
393	389 392	mpbird	$⊢ (φ \land x \in A) \to S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}]$
394	393	unissd	$⊢ (φ \land x \in A) \to ⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}] \subseteq ⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}]$
395		imassrn	$⊢ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \subseteq ran (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
396	395 267	sstrid	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \subseteq 𝒫 {Base}_{G}$
397		sspwuni	$⊢ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \subseteq {Base}_{G}$
398	396 397	sylib	$⊢ (φ \land x \in A) \to ⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}] \subseteq {Base}_{G}$
399	166 6 394 398	mrcssd	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq K (⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
400		ss2in	$⊢ (S (x) \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) \land K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq K (⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])) \to S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) \cap K (⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
401	345 399 400	syl2anc	$⊢ (φ \land x \in A) \to S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) \cap K (⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}])$
402	58	a1i	$⊢ (φ \land x \in A) \to dom (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) = A [\{1^{st} (x)\}]$
403	53 402 69 8 6	dprddisj	$⊢ (φ \land x \in A) \to (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) (2^{nd} (x)) \cap K (⋃ (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) [A [\{1^{st} (x)\}] ∖ \{2^{nd} (x)\}]) = \{0_{G}\}$
404	401 403	sseqtrd	$⊢ (φ \land x \in A) \to S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \subseteq \{0_{G}\}$
405	8	subg0cl	$⊢ K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \in SubGrp (G) \to 0_{G} \in K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}])$
406	222 405	syl	$⊢ (φ \land x \in A) \to 0_{G} \in K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}])$
407	333 406	elind	$⊢ (φ \land x \in A) \to 0_{G} \in (S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]))$
408	407	snssd	$⊢ (φ \land x \in A) \to \{0_{G}\} \subseteq S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}])$
409	404 408	eqssd	$⊢ (φ \land x \in A) \to S (x) \cap K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) = \{0_{G}\}$
410	340 409	syl5eq	$⊢ (φ \land x \in A) \to K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) \cap S (x) = \{0_{G}\}$
411	225 222 310 224 8 339 410	lsmdisj2	$⊢ (φ \land x \in A) \to S (x) \cap (K (⋃ S [({A ↾}_{\{1^{st} (x)\}}) ∖ \{x\}]) LSSum (G) K (⋃ S [{A ↾}_{(I ∖ \{1^{st} (x)\})}])) = \{0_{G}\}$
412	309 411	sseqtrd	$⊢ (φ \land x \in A) \to S (x) \cap K (⋃ S [A ∖ \{x\}]) \subseteq \{0_{G}\}$
413	7 8 6 10 41 2 162 412	dmdprdd	$⊢ φ \to G dom DProd S$

Metamath Proof Explorer

Theorem dprd2da

Proof