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 20115

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 20078	. . 3 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
6	4, 5	syl 18	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		resiun2 6001	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖})
8		iunid 5026	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼
9	8	reseq2i 5977	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼)
10	7, 9	eqtr3i 2788	. . . 4 ⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼)
11		dprd2d.1	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
12		dprd2d.3	. . . . 5 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)
13		relssres 6023	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴)
14	11, 12, 13	syl2anc 595	. . . 4 ⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴)
15	10, 14	eqtrid 2810	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16		ovex 7445	. . . . . 6 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17		eqid 2763	. . . . . 6 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
18	16, 17	dmmpti 6681	. . . . 5 ⊢ dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19		reldmdprd 20070	. . . . . . 7 ⊢ Rel dom DProd
20	19	brrelex2i 5720	. . . . . 6 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21		dmexg 7899	. . . . . 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 6288	. . . . . 6 ⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25		vsnex 5408	. . . . . . 7 ⊢ {𝑖} ∈ V
26		ovex 7445	. . . . . . . . 9 ⊢ (𝑖𝑆𝑗) ∈ V
27		eqid 2763	. . . . . . . . 9 ⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
28	26, 27	dmmpti 6681	. . . . . . . 8 ⊢ dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29		dprd2d.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30	19	brrelex2i 5720	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31		dmexg 7899	. . . . . . . . 9 ⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
32	29, 30, 31	3syl 19	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
33	28, 32	eqeltrrid 2868	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V)
34		xpexg 7750	. . . . . . 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 7961	. . . 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 4600	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → {𝑖} = {(1^st ‘𝑥)})
43	42	imaeq2d 6064	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑥)}))
44		oveq1 7419	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑖𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑗))
45	43, 44	mpteq12dv 5199	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
46	45	breq2d 5122	. . . . . . . 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 8038	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
51	11, 50	sylan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
52	49, 51	sseldd 3939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ 𝐼)
53	46, 48, 52	rspcdva 3583	. . . . . . 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 7445	. . . . . . 7 ⊢ ((1^st ‘𝑥)𝑆𝑗) ∈ V
57		eqid 2763	. . . . . . 7 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
58	56, 57	dmmpti 6681	. . . . . 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 8037	. . . . . . . . . . 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 5111	. . . . . . . . 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 6090	. . . . . . . . 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 8037	. . . . . . . . . . 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 5111	. . . . . . . . 9 ⊢ ((1^st ‘𝑦)𝐴(2^nd ‘𝑦) ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
78	76, 77	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦)𝐴(2^nd ‘𝑦))
79		elrelimasn 6090	. . . . . . . . 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 4602	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → {(1^st ‘𝑥)} = {(1^st ‘𝑦)})
85	84	imaeq2d 6064	. . . . . 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 6896	. . . . . . . . . 10 ⊢ (1^st ‘𝑥) ∈ V
92		fvex 6896	. . . . . . . . . 10 ⊢ (2^nd ‘𝑥) ∈ V
93	91, 92	opth 5460	. . . . . . . . 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 20081	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))))
99		df-ov 7415	. . . . . 6 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
100		oveq2 7420	. . . . . . . 8 ⊢ (𝑗 = (2^nd ‘𝑥) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
101	100, 57, 56	fvmpt3i 6997	. . . . . . 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 6887	. . . . . 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 7427	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
107	85, 106	mpteq12dv 5199	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
108	107	fveq1d 6885	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)))
109		df-ov 7415	. . . . . . . 8 ⊢ ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
110		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑦)𝑆𝑗) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
111		eqid 2763	. . . . . . . . . 10 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))
112		ovex 7445	. . . . . . . . . 10 ⊢ ((1^st ‘𝑦)𝑆𝑗) ∈ V
113	110, 111, 112	fvmpt3i 6997	. . . . . . . . 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 6887	. . . . . . . 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 6887	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦)))
120	98, 105, 119	3sstr3d 3992	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
121	11, 41, 12, 29, 4, 3	dprd2dlem2 20113	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
122	45	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
123	122, 17, 16	fvmpt3i 6997	. . . . . . . 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 3975	. . . . . 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 8038	. . . . . . . . 9 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → (1^st ‘𝑦) ∈ dom 𝐴)
134	72, 73, 133	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ dom 𝐴)
135	132, 134	sseldd 3939	. . . . . . 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 20081	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))))
139		sneq 4600	. . . . . . . . . . . . 13 ⊢ (𝑖 = (1^st ‘𝑦) → {𝑖} = {(1^st ‘𝑦)})
140	139	imaeq2d 6064	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑦)}))
141		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑖𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
142	140, 141	mpteq12dv 5199	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
143	142	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
144	143, 17, 16	fvmpt3i 6997	. . . . . . . . 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 6887	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))))
147		eqid 2763	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
148	147	dprdssv 20089	. . . . . . . 8 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149	142	breq2d 5122	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
150	47	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151	149, 150, 135	rspcdva 3583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
152	112, 111	dmmpti 6681	. . . . . . . . . . 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 20098	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
155	116, 154	eqsstrrd 3973	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
156	147, 1	cntz2ss 19406	. . . . . . . 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 3972	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
159	158	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
160	138, 159	sstrd 3948	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
161	127, 160	sstrd 3948	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
162	120, 161	pm2.61dane 3045	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
163	6	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp)
164	147	subgacs 19228	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165		acsmre 17709	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166	163, 164, 165	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
167	14	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴)
168		undif2 4439	. . . . . . . . . . . . . . . . . 18 ⊢ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})) = ({(1^st ‘𝑥)} ∪ 𝐼)
169	52	snssd 4753	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1^st ‘𝑥)} ⊆ 𝐼)
170		ssequn1 4140	. . . . . . . . . . . . . . . . . . 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 5980	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
174	167, 173	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
175		resundi 5994	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))) = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
176	174, 175	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
177	176	difeq1d 4081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}))
178		difundir 4245	. . . . . . . . . . . . 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 5111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
183	92	brresi 5989	. . . . . . . . . . . . . . . . . . . . 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 4759	. . . . . . . . . . . . . . . . . . . 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 4678	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
191	189, 190	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅)
192		disj3 4415	. . . . . . . . . . . . . . 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 4123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
196	179, 195	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
197	196	imaeq2d 6064	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
198		imaundi 6149	. . . . . . . . . 10 ⊢ (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
199	197, 198	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
200	199	unieqd 4886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
201		uniun 4896	. . . . . . . 8 ⊢ ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
202	200, 201	eqtrdi 2814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
203		imassrn 6075	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
204	41	frnd 6716	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205	204	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206		mresspw 17645	. . . . . . . . . . . . 13 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207	166, 206	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208	205, 207	sstrd 3948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209	203, 208	sstrid 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210		sspwuni 5067	. . . . . . . . . 10 ⊢ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211	209, 210	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212	166, 3, 211	mrcssidd 17682	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
213		imassrn 6075	. . . . . . . . . . 11 ⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ ran 𝑆
214	213, 208	sstrid 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215		sspwuni 5067	. . . . . . . . . 10 ⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
216	214, 215	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
217	166, 3, 216	mrcssidd 17682	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
218		unss12 4142	. . . . . . . 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 3972	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
221	3	mrccl 17668	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222	166, 211, 221	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
223	3	mrccl 17668	. . . . . . . 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 19730	. . . . . . 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 3948	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
229		difss 4091	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1^st ‘𝑥)})
230		ressn 6288	. . . . . . . . . . . . 13 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) = ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
231	229, 230	sseqtri 3986	. . . . . . . . . . . 12 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
232		imass2 6106	. . . . . . . . . . . 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 7445	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝑆𝑖) ∈ V
235		oveq2 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑖))
236	57, 235	elrnmpt1s 5951	. . . . . . . . . . . . . . . 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 7419	. . . . . . . . . . . . . . . 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 4648	. . . . . . . . . . . . 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 6712	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆)
247		resss 6002	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) ⊆ 𝐴
248	230, 247	eqsstrri 3985	. . . . . . . . . . . . . 14 ⊢ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ 𝐴
249	245	fdmd 6718	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴)
250	248, 249	sseqtrrid 3981	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ dom 𝑆)
251		funimassov 7589	. . . . . . . . . . . . 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 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
255	254	unissd 4883	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
256		df-ov 7415	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑥)𝑆𝑗) = (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩)
257	41	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258		elrelimasn 6090	. . . . . . . . . . . . . . . . . 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 5111	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝐴𝑗 ↔ ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
262	260, 261	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
263	257, 262	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
264	256, 263	eqeltrid 2867	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ((1^st ‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265	264	fmpttd 7112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺))
266	265	frnd 6716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267	266, 207	sstrd 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268		sspwuni 5067	. . . . . . . . . 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 17681	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
271	3	dprdspan 20100	. . . . . . . . 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 3975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
274	16, 17	fnmpti 6680	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275		fnressn 7157	. . . . . . . . . . . . 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 4846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩ = ⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩)
278	277	sneqd 4602	. . . . . . . . . . . 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 7428	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}))
281		dprdsubg 20097	. . . . . . . . . . . . 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 20109	. . . . . . . . . . . 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 4091	. . . . . . . . . . 11 ⊢ (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼
290	289	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼)
291		disjdif 4434	. . . . . . . . . . 11 ⊢ ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅
292	291	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅)
293	287, 288, 169, 290, 292, 1	dprdcntz2 20111	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
294	286, 293	eqsstrrd 3973	. . . . . . . 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 20114	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297		resmpt 6041	. . . . . . . . . . . 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 7423	. . . . . . . . . 10 ⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300	296, 299	eqtr4di 2816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
301	300	fveq2d 6887	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
302	294, 301	sseqtrrd 3975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
303	273, 302	sstrd 3948	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
304	225, 1	lsmsubg 19725	. . . . . 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 17677	. . . . 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 4196	. . . 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 7081	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺))
311	225	lsmlub 19735	. . . . . . . . . 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 3975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
315	287, 288, 290	dprdres 20101	. . . . . . . . . . . 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 20100	. . . . . . . . . . 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 5676	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
320	319	unieqi 4885	. . . . . . . . . . 11 ⊢ ∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
321	320	fveq2i 6886	. . . . . . . . . 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 3996	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
325	323, 324	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
326		ss2in 4198	. . . . . . 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 20082	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) = {(0_g‘𝐺)})
329	327, 328	sseqtrd 3974	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ {(0_g‘𝐺)})
330	225	lsmub2 19729	. . . . . . . . 9 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
331	222, 310, 330	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
332	2	subg0cl 19201	. . . . . . . . 9 ⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
333	310, 332	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
334	331, 333	sseldd 3939	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
335	2	subg0cl 19201	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
336	224, 335	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
337	334, 336	elind 4154	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
338	337	snssd 4753	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
339	329, 338	eqssd 3955	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = {(0_g‘𝐺)})
340		incom 4163	. . . . 5 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
341	69, 101	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
342	61	fveq2d 6887	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
343	99, 341, 342	3eqtr4a 2824	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
344		eqimss2 3997	. . . . . . . . 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 4754	. . . . . . . . . . . . 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 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴)
350	347, 349, 74	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
351	350	fveq2d 6887	. . . . . . . . . . . . . . . . . 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 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑦) ∈ V
355	354	opelresi 5988	. . . . . . . . . . . . . . . . . . . . 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 4607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} → (1^st ‘𝑦) = (1^st ‘𝑥))
359	357, 358	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) = (1^st ‘𝑥))
360	359	oveq1d 7427	. . . . . . . . . . . . . . . . 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 8020	. . . . . . . . . . . . . . . . . . 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 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑦) ∈ V
369	368, 354	opth 5460	. . . . . . . . . . . . . . . . . . . . . . 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 4754	. . . . . . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ V
378		difss 4091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)})
379		resmpt 6041	. . . . . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
382	380, 381	elrnmpt1s 5951	. . . . . . . . . . . . . . . . 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 5676	. . . . . . . . . . . . . . 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 3949	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391		funimass4 6947	. . . . . . . . . . . 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 4883	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
395		imassrn 6075	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
396	395, 267	sstrid 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397		sspwuni 5067	. . . . . . . . . 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 17681	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
400		ss2in 4198	. . . . . . . 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 20082	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))) = {(0_g‘𝐺)})
404	401, 403	sseqtrd 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
405	2	subg0cl 19201	. . . . . . . . 9 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
406	222, 405	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
407	333, 406	elind 4154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
408	407	snssd 4753	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
409	404, 408	eqssd 3955	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) = {(0_g‘𝐺)})
410	340, 409	eqtrid 2810	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0_g‘𝐺)})
411	225, 222, 310, 224, 2, 339, 410	lsmdisj2 19753	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) = {(0_g‘𝐺)})
412	309, 411	sseqtrd 3974	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
413	1, 2, 3, 6, 40, 41, 162, 412	dmdprdd 20072	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 Vcvv 3455 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 𝒫 cpw 4563 {csn 4590 ⟨cop 4596 ∪ cuni 4873 ∪ ciun 4957 class class class wbr 5110 ↦ cmpt 5193 × cxp 5661 dom cdm 5663 ran crn 5664 ↾ cres 5665 “ cima 5666 Rel wrel 5668 Fun wfun 6532 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7412 1^st c1st 7985 2^nd c2nd 7986 Basecbs 17270 0_gc0g 17493 Moorecmre 17635 mrClscmrc 17636 ACScacs 17638 Grpcgrp 19001 SubGrpcsubg 19187 Cntzccntz 19386 LSSumclsm 19705 DProd cdprd 20066

This theorem was proved from 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 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem 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 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8158 df-tpos 8223 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-ixp 8897 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-fsupp 9323 df-oi 9473 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-n0 12506 df-z 12593 df-uz 12864 df-fz 13537 df-fzo 13685 df-seq 14040 df-hash 14369 df-sets 17225 df-slot 17243 df-ndx 17255 df-base 17271 df-ress 17292 df-plusg 17324 df-0g 17495 df-gsum 17496 df-mre 17639 df-mrc 17640 df-acs 17642 df-mgm 18699 df-sgrp 18778 df-mnd 18794 df-mhm 18842 df-submnd 18843 df-grp 19004 df-minusg 19005 df-sbg 19006 df-mulg 19135 df-subg 19190 df-ghm 19285 df-gim 19330 df-cntz 19388 df-oppg 19417 df-lsm 19707 df-cmn 19853 df-dprd 20068

This theorem is referenced by: dprd2db 20116 dprd2d2 20117

W3C validator