dprd2da - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dprd2da		Structured version Visualization version GIF version

Theorem dprd2da 20118

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

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

**Assertion**
Ref	Expression
dprd2da	⊢ (𝜑 → 𝐺dom DProd 𝑆)

Distinct variable groups: 𝑖,𝑗,𝐴 𝑖,𝐺,𝑗 𝑖,𝐼 𝑖,𝐾 𝜑,𝑖,𝑗 𝑆,𝑖,𝑗 Allowed substitution hints: 𝐼(𝑗) 𝐾(𝑗)

Proof of Theorem dprd2da Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2763	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		dprd2d.k	. 2 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))
4		dprd2d.5	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5		dprdgrp 20081	. . 3 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
6	4, 5	syl 18	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		resiun2 5999	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖})
8		iunid 5025	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼
9	8	reseq2i 5975	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼)
10	7, 9	eqtr3i 2788	. . . 4 ⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼)
11		dprd2d.1	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
12		dprd2d.3	. . . . 5 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)
13		relssres 6021	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴)
14	11, 12, 13	syl2anc 595	. . . 4 ⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴)
15	10, 14	eqtrid 2810	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16		ovex 7443	. . . . . 6 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17		eqid 2763	. . . . . 6 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
18	16, 17	dmmpti 6679	. . . . 5 ⊢ dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19		reldmdprd 20073	. . . . . . 7 ⊢ Rel dom DProd
20	19	brrelex2i 5718	. . . . . 6 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21		dmexg 7894	. . . . . 6 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
22	4, 20, 21	3syl 19	. . . . 5 ⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
23	18, 22	eqeltrrid 2868	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
24		ressn 6286	. . . . . 6 ⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25		vsnex 5406	. . . . . . 7 ⊢ {𝑖} ∈ V
26		ovex 7443	. . . . . . . . 9 ⊢ (𝑖𝑆𝑗) ∈ V
27		eqid 2763	. . . . . . . . 9 ⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
28	26, 27	dmmpti 6679	. . . . . . . 8 ⊢ dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29		dprd2d.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30	19	brrelex2i 5718	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31		dmexg 7894	. . . . . . . . 9 ⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
32	29, 30, 31	3syl 19	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
33	28, 32	eqeltrrid 2868	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V)
34		xpexg 7745	. . . . . . 7 ⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
35	25, 33, 34	sylancr 598	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
36	24, 35	eqeltrid 2867	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
37	36	ralrimiva 3157	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38		iunexg 7956	. . . 4 ⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
39	23, 37, 38	syl2anc 595	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
40	15, 39	eqeltrrd 2864	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
41		dprd2d.2	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
42		sneq 4599	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → {𝑖} = {(1^st ‘𝑥)})
43	42	imaeq2d 6062	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑥)}))
44		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑖𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑗))
45	43, 44	mpteq12dv 5198	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
46	45	breq2d 5121	. . . . . . . 8 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
47	29	ralrimiva 3157	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48	47	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
49	12	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼)
50		1stdm 8033	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
51	11, 50	sylan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
52	49, 51	sseldd 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ 𝐼)
53	46, 48, 52	rspcdva 3582	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
54	53	3ad2antr1 1207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
55	54	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
56		ovex 7443	. . . . . . 7 ⊢ ((1^st ‘𝑥)𝑆𝑗) ∈ V
57		eqid 2763	. . . . . . 7 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
58	56, 57	dmmpti 6679	. . . . . 6 ⊢ dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)})
59	58	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)}))
60		1st2nd 8032	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
61	11, 60	sylan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
62		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
63	61, 62	eqeltrrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
64		df-br 5110	. . . . . . . . 9 ⊢ ((1^st ‘𝑥)𝐴(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
65	63, 64	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥)𝐴(2^nd ‘𝑥))
66	11	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴)
67		elrelimasn 6088	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
68	66, 67	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
69	65, 68	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
70	69	3ad2antr1 1207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
71	70	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
72	11	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴)
73		simpr2 1214	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴)
74		1st2nd 8032	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
75	72, 73, 74	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
76	75, 73	eqeltrrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
77		df-br 5110	. . . . . . . . 9 ⊢ ((1^st ‘𝑦)𝐴(2^nd ‘𝑦) ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
78	76, 77	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦)𝐴(2^nd ‘𝑦))
79		elrelimasn 6088	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
80	72, 79	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
81	78, 80	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
82	81	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
83		simpr 489	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (1^st ‘𝑥) = (1^st ‘𝑦))
84	83	sneqd 4601	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → {(1^st ‘𝑥)} = {(1^st ‘𝑦)})
85	84	imaeq2d 6062	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝐴 “ {(1^st ‘𝑥)}) = (𝐴 “ {(1^st ‘𝑦)}))
86	82, 85	eleqtrrd 2866	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
87		simplr3 1236	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝑥 ≠ 𝑦)
88		simpr1 1213	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴)
89	72, 88, 60	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
90	89, 75	eqeq12d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
91		fvex 6894	. . . . . . . . . 10 ⊢ (1^st ‘𝑥) ∈ V
92		fvex 6894	. . . . . . . . . 10 ⊢ (2^nd ‘𝑥) ∈ V
93	91, 92	opth 5458	. . . . . . . . 9 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
94	90, 93	bitrdi 290	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦))))
95	94	baibd 548	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
96	95	necon3bid 3002	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2^nd ‘𝑥) ≠ (2^nd ‘𝑦)))
97	87, 96	mpbid 235	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ≠ (2^nd ‘𝑦))
98	55, 59, 71, 86, 97, 1	dprdcntz 20084	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))))
99		df-ov 7413	. . . . . 6 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
100		oveq2 7418	. . . . . . . 8 ⊢ (𝑗 = (2^nd ‘𝑥) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
101	100, 57, 56	fvmpt3i 6995	. . . . . . 7 ⊢ ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
102	70, 101	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
103	89	fveq2d 6885	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
104	99, 102, 103	3eqtr4a 2824	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
105	104	adantr 485	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
106	83	oveq1d 7425	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
107	85, 106	mpteq12dv 5198	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
108	107	fveq1d 6883	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)))
109		df-ov 7413	. . . . . . . 8 ⊢ ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
110		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑦)𝑆𝑗) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
111		eqid 2763	. . . . . . . . . 10 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))
112		ovex 7443	. . . . . . . . . 10 ⊢ ((1^st ‘𝑦)𝑆𝑗) ∈ V
113	110, 111, 112	fvmpt3i 6995	. . . . . . . . 9 ⊢ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
114	81, 113	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
115	75	fveq2d 6885	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
116	109, 114, 115	3eqtr4a 2824	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
117	116	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
118	108, 117	eqtrd 2798	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
119	118	fveq2d 6885	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦)))
120	98, 105, 119	3sstr3d 3991	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
121	11, 41, 12, 29, 4, 3	dprd2dlem2 20116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
122	45	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
123	122, 17, 16	fvmpt3i 6995	. . . . . . . 8 ⊢ ((1^st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
124	52, 123	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
125	121, 124	sseqtrrd 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
126	125	3ad2antr1 1207	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
127	126	adantr 485	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
128	4	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
129	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
130	52	3ad2antr1 1207	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
131	130	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
132	12	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼)
133		1stdm 8033	. . . . . . . . 9 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → (1^st ‘𝑦) ∈ dom 𝐴)
134	72, 73, 133	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ dom 𝐴)
135	132, 134	sseldd 3938	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
136	135	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
137		simpr 489	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ≠ (1^st ‘𝑦))
138	128, 129, 131, 136, 137, 1	dprdcntz 20084	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))))
139		sneq 4599	. . . . . . . . . . . . 13 ⊢ (𝑖 = (1^st ‘𝑦) → {𝑖} = {(1^st ‘𝑦)})
140	139	imaeq2d 6062	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑦)}))
141		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑖𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
142	140, 141	mpteq12dv 5198	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
143	142	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
144	143, 17, 16	fvmpt3i 6995	. . . . . . . . 9 ⊢ ((1^st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
145	135, 144	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
146	145	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))))
147		eqid 2763	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
148	147	dprdssv 20092	. . . . . . . 8 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149	142	breq2d 5121	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
150	47	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151	149, 150, 135	rspcdva 3582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
152	112, 111	dmmpti 6679	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑦)})
153	152	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑦)}))
154	151, 153, 81	dprdub 20101	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
155	116, 154	eqsstrrd 3972	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
156	147, 1	cntz2ss 19409	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
157	148, 155, 156	sylancr 598	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
158	146, 157	eqsstrd 3971	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
159	158	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
160	138, 159	sstrd 3947	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
161	127, 160	sstrd 3947	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
162	120, 161	pm2.61dane 3045	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
163	6	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp)
164	147	subgacs 19231	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165		acsmre 17712	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166	163, 164, 165	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
167	14	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴)
168		undif2 4438	. . . . . . . . . . . . . . . . . 18 ⊢ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})) = ({(1^st ‘𝑥)} ∪ 𝐼)
169	52	snssd 4752	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1^st ‘𝑥)} ⊆ 𝐼)
170		ssequn1 4139	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(1^st ‘𝑥)} ⊆ 𝐼 ↔ ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
171	169, 170	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
172	168, 171	eqtr2id 2811	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})))
173	172	reseq2d 5978	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
174	167, 173	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
175		resundi 5992	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))) = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
176	174, 175	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
177	176	difeq1d 4080	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}))
178		difundir 4244	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
179	177, 178	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})))
180		neirr 2967	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (1^st ‘𝑥) ≠ (1^st ‘𝑥)
181	61	eleq1d 2848	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
182		df-br 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
183	92	brresi 5987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ∧ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
184	183	simplbi 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}))
185		eldifsni 4758	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
186	184, 185	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
187	182, 186	sylbir 238	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
188	181, 187	biimtrdi 256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥)))
189	180, 188	mtoi 202	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
190		disjsn 4677	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
191	189, 190	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅)
192		disj3 4414	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
193	191, 192	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
194	193	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
195	194	uneq2d 4122	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
196	179, 195	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
197	196	imaeq2d 6062	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
198		imaundi 6147	. . . . . . . . . 10 ⊢ (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
199	197, 198	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
200	199	unieqd 4885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
201		uniun 4895	. . . . . . . 8 ⊢ ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
202	200, 201	eqtrdi 2814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
203		imassrn 6073	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
204	41	frnd 6714	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205	204	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206		mresspw 17648	. . . . . . . . . . . . 13 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207	166, 206	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208	205, 207	sstrd 3947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209	203, 208	sstrid 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210		sspwuni 5066	. . . . . . . . . 10 ⊢ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211	209, 210	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212	166, 3, 211	mrcssidd 17685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
213		imassrn 6073	. . . . . . . . . . 11 ⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ ran 𝑆
214	213, 208	sstrid 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215		sspwuni 5066	. . . . . . . . . 10 ⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
216	214, 215	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
217	166, 3, 216	mrcssidd 17685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
218		unss12 4141	. . . . . . . 8 ⊢ ((∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
219	212, 217, 218	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
220	202, 219	eqsstrd 3971	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
221	3	mrccl 17671	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222	166, 211, 221	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
223	3	mrccl 17671	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
224	166, 216, 223	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
225		eqid 2763	. . . . . . . 8 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
226	225	lsmunss 19733	. . . . . . 7 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
227	222, 224, 226	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
228	220, 227	sstrd 3947	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
229		difss 4090	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1^st ‘𝑥)})
230		ressn 6286	. . . . . . . . . . . . 13 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) = ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
231	229, 230	sseqtri 3985	. . . . . . . . . . . 12 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
232		imass2 6104	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))))
233	231, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
234		ovex 7443	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝑆𝑖) ∈ V
235		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑖))
236	57, 235	elrnmpt1s 5949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ ((1^st ‘𝑥)𝑆𝑖) ∈ V) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
237	234, 236	mpan2 703	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
238	237	rgen 3081	. . . . . . . . . . . . . 14 ⊢ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
239	238	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
240		oveq1 7417	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (1^st ‘𝑥) → (𝑦𝑆𝑖) = ((1^st ‘𝑥)𝑆𝑖))
241	240	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (1^st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
242	241	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (1^st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
243	91, 242	ralsn 4647	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
244	239, 243	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
245	41	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
246	245	ffund 6710	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆)
247		resss 6000	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) ⊆ 𝐴
248	230, 247	eqsstrri 3984	. . . . . . . . . . . . . 14 ⊢ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ 𝐴
249	245	fdmd 6716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴)
250	248, 249	sseqtrrid 3980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ dom 𝑆)
251		funimassov 7587	. . . . . . . . . . . . 13 ⊢ ((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 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
253	244, 252	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
254	233, 253	sstrid 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
255	254	unissd 4882	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
256		df-ov 7413	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑥)𝑆𝑗) = (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩)
257	41	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258		elrelimasn 6088	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
259	66, 258	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
260	259	biimpa 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (1^st ‘𝑥)𝐴𝑗)
261		df-br 5110	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝐴𝑗 ↔ ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
262	260, 261	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
263	257, 262	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
264	256, 263	eqeltrid 2867	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ((1^st ‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265	264	fmpttd 7110	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺))
266	265	frnd 6714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267	266, 207	sstrd 3947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268		sspwuni 5066	. . . . . . . . . 10 ⊢ (ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
269	267, 268	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
270	166, 3, 255, 269	mrcssd 17684	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
271	3	dprdspan 20103	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
272	53, 271	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
273	270, 272	sseqtrrd 3974	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
274	16, 17	fnmpti 6678	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275		fnressn 7155	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1^st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
276	274, 52, 275	sylancr 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
277	124	opeq2d 4845	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩ = ⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩)
278	277	sneqd 4601	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩} = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
279	276, 278	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
280	279	oveq2d 7426	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}))
281		dprdsubg 20100	. . . . . . . . . . . . 13 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
282	53, 281	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
283		dprdsn 20112	. . . . . . . . . . . 12 ⊢ (((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 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺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 500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
286	280, 285	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
287	4	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
288	18	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
289		difss 4090	. . . . . . . . . . 11 ⊢ (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼
290	289	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼)
291		disjdif 4433	. . . . . . . . . . 11 ⊢ ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅
292	291	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅)
293	287, 288, 169, 290, 292, 1	dprdcntz2 20114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
294	286, 293	eqsstrrd 3972	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
295	29	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
296	66, 245, 49, 295, 287, 3, 290	dprd2dlem1 20117	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297		resmpt 6039	. . . . . . . . . . . 12 ⊢ ((𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
298	289, 297	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
299	298	oveq2i 7421	. . . . . . . . . 10 ⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300	296, 299	eqtr4di 2816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
301	300	fveq2d 6885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
302	294, 301	sseqtrrd 3974	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
303	273, 302	sstrd 3947	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
304	225, 1	lsmsubg 19728	. . . . . 6 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
305	222, 224, 303, 304	syl3anc 1398	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
306	3	mrcsscl 17680	. . . . 5 ⊢ (((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 1398	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
308		sslin 4195	. . . 4 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
309	307, 308	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
310	41	ffvelcdmda 7079	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺))
311	225	lsmlub 19738	. . . . . . . . . 10 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(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 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(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 724	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
314	313, 124	sseqtrrd 3974	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
315	287, 288, 290	dprdres 20104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
316	315	simpld 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
317	3	dprdspan 20103	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
318	316, 317	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
319		df-ima 5674	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
320	319	unieqi 4884	. . . . . . . . . . 11 ⊢ ∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
321	320	fveq2i 6884	. . . . . . . . . 10 ⊢ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
322	318, 321	eqtr4di 2816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
323	300, 322	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
324		eqimss 3995	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
325	323, 324	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
326		ss2in 4197	. . . . . . 7 ⊢ ((((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(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 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))))
328	287, 288, 52, 2, 3	dprddisj 20085	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) = {(0_g‘𝐺)})
329	327, 328	sseqtrd 3973	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ {(0_g‘𝐺)})
330	225	lsmub2 19732	. . . . . . . . 9 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
331	222, 310, 330	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
332	2	subg0cl 19204	. . . . . . . . 9 ⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
333	310, 332	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
334	331, 333	sseldd 3938	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
335	2	subg0cl 19204	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
336	224, 335	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
337	334, 336	elind 4153	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
338	337	snssd 4752	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
339	329, 338	eqssd 3954	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = {(0_g‘𝐺)})
340		incom 4162	. . . . 5 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
341	69, 101	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
342	61	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
343	99, 341, 342	3eqtr4a 2824	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
344		eqimss2 3996	. . . . . . . . 9 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
345	343, 344	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
346		eldifsn 4753	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥))
347	11	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴)
348		simprl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
349	247, 348	sselid 3935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴)
350	347, 349, 74	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
351	350	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
352	351, 109	eqtr4di 2816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
353	350, 348	eqeltrrd 2864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
354		fvex 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑦) ∈ V
355	354	opelresi 5986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ↔ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} ∧ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴))
356	355	simplbi 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
357	353, 356	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
358		elsni 4606	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} → (1^st ‘𝑦) = (1^st ‘𝑥))
359	357, 358	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) = (1^st ‘𝑥))
360	359	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
361	352, 360	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
362	348, 230	eleqtrdi 2873	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
363		xp2nd 8015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
364	362, 363	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
365		simprr 784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥)
366	61	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
367	350, 366	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
368		fvex 6894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑦) ∈ V
369	368, 354	opth 5458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ ((1^st ‘𝑦) = (1^st ‘𝑥) ∧ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
370	369	baib 544	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1^st ‘𝑦) = (1^st ‘𝑥) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
371	359, 370	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
372	367, 371	bitrd 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
373	372	necon3bid 3002	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
374	365, 373	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ≠ (2^nd ‘𝑥))
375		eldifsn 4753	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↔ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
376	364, 374, 375	sylanbrc 594	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
377		ovex 7443	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ V
378		difss 4090	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)})
379		resmpt 6039	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 “ {(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 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
381		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
382	380, 381	elrnmpt1s 5949	. . . . . . . . . . . . . . . . 17 ⊢ (((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 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
384	361, 383	eqeltrd 2863	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
385		df-ima 5674	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
386	384, 385	eleqtrrdi 2874	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
387	386	ex 417	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
388	346, 387	biimtrid 245	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
389	388	ralrimiv 3156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
390	231, 250	sstrid 3948	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391		funimass4 6945	. . . . . . . . . . . 12 ⊢ ((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 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
393	389, 392	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
394	393	unissd 4882	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
395		imassrn 6073	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
396	395, 267	sstrid 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397		sspwuni 5066	. . . . . . . . . 10 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
398	396, 397	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
399	166, 3, 394, 398	mrcssd 17684	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
400		ss2in 4197	. . . . . . . 8 ⊢ (((𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(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 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))))
402	58	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)}))
403	53, 402, 69, 2, 3	dprddisj 20085	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))) = {(0_g‘𝐺)})
404	401, 403	sseqtrd 3973	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
405	2	subg0cl 19204	. . . . . . . . 9 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
406	222, 405	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
407	333, 406	elind 4153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
408	407	snssd 4752	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
409	404, 408	eqssd 3954	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) = {(0_g‘𝐺)})
410	340, 409	eqtrid 2810	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0_g‘𝐺)})
411	225, 222, 310, 224, 2, 339, 410	lsmdisj2 19756	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) = {(0_g‘𝐺)})
412	309, 411	sseqtrd 3973	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
413	1, 2, 3, 6, 40, 41, 162, 412	dmdprdd 20075	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 Vcvv 3455 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4562 {csn 4589 ⟨cop 4595 ∪ cuni 4872 ∪ ciun 4956 class class class wbr 5109 ↦ cmpt 5192 × cxp 5659 dom cdm 5661 ran crn 5662 ↾ cres 5663 “ cima 5664 Rel wrel 5666 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 1^st c1st 7980 2^nd c2nd 7981 Basecbs 17273 0_gc0g 17496 Moorecmre 17638 mrClscmrc 17639 ACScacs 17641 Grpcgrp 19004 SubGrpcsubg 19190 Cntzccntz 19389 LSSumclsm 19708 DProd cdprd 20069

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-tpos 8218 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-map 8822 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-oi 9468 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-nn 12238 df-2 12307 df-n0 12509 df-z 12596 df-uz 12867 df-fz 13540 df-fzo 13688 df-seq 14043 df-hash 14372 df-sets 17228 df-slot 17246 df-ndx 17258 df-base 17274 df-ress 17295 df-plusg 17327 df-0g 17498 df-gsum 17499 df-mre 17642 df-mrc 17643 df-acs 17645 df-mgm 18702 df-sgrp 18781 df-mnd 18797 df-mhm 18845 df-submnd 18846 df-grp 19007 df-minusg 19008 df-sbg 19009 df-mulg 19138 df-subg 19193 df-ghm 19288 df-gim 19333 df-cntz 19391 df-oppg 19420 df-lsm 19710 df-cmn 19856 df-dprd 20071

This theorem is used by: dprd2db 20119 dprd2d2 20120

W3C validator