dprd2da

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

	Ref	Expression
Hypotheses	dprd2d.1	\|- ( ph -> Rel A )
	dprd2d.2	\|- ( ph -> S : A --> ( SubGrp ` G ) )
	dprd2d.3	\|- ( ph -> dom A C_ I )
	dprd2d.4	\|- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) \|-> ( i S j ) ) )
	dprd2d.5	\|- ( ph -> G dom DProd ( i e. I \|-> ( G DProd ( j e. ( A " { i } ) \|-> ( i S j ) ) ) ) )
	dprd2d.k	\|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion	dprd2da	\|- ( ph -> G dom DProd S )

Proof

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

Metamath Proof Explorer

Theorem dprd2da

Proof