dprd2da

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

	Ref	Expression
Hypotheses	dprd2d.1	⊢ ( 𝜑 → Rel 𝐴 )
	dprd2d.2	⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
	dprd2d.3	⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐼 )
	dprd2d.4	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
	dprd2d.5	⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
	dprd2d.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion	dprd2da	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )

Proof

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

Metamath Proof Explorer

Theorem dprd2da

Proof