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 18441

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 2622	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2622	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		dprd2d.k	. 2 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))
4		dprd2d.5	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5		dprdgrp 18404	. . 3 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		resiun2 5418	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖})
8		iunid 4575	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼
9	8	reseq2i 5393	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼)
10	7, 9	eqtr3i 2646	. . . 4 ⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼)
11		dprd2d.1	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
12		dprd2d.3	. . . . 5 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)
13		relssres 5437	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴)
14	11, 12, 13	syl2anc 693	. . . 4 ⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴)
15	10, 14	syl5eq 2668	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16		ovex 6678	. . . . . 6 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17		eqid 2622	. . . . . 6 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
18	16, 17	dmmpti 6023	. . . . 5 ⊢ dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19		reldmdprd 18396	. . . . . . 7 ⊢ Rel dom DProd
20	19	brrelex2i 5159	. . . . . 6 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21		dmexg 7097	. . . . . 6 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
22	4, 20, 21	3syl 18	. . . . 5 ⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
23	18, 22	syl5eqelr 2706	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
24		ressn 5671	. . . . . 6 ⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25		snex 4908	. . . . . . 7 ⊢ {𝑖} ∈ V
26		ovex 6678	. . . . . . . . 9 ⊢ (𝑖𝑆𝑗) ∈ V
27		eqid 2622	. . . . . . . . 9 ⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
28	26, 27	dmmpti 6023	. . . . . . . 8 ⊢ dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29		dprd2d.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30	19	brrelex2i 5159	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31		dmexg 7097	. . . . . . . . 9 ⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
32	29, 30, 31	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
33	28, 32	syl5eqelr 2706	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V)
34		xpexg 6960	. . . . . . 7 ⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
35	25, 33, 34	sylancr 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
36	24, 35	syl5eqel 2705	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
37	36	ralrimiva 2966	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38		iunexg 7143	. . . 4 ⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
39	23, 37, 38	syl2anc 693	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
40	15, 39	eqeltrrd 2702	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
41		dprd2d.2	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
42	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼)
43		1stdm 7215	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
44	11, 43	sylan 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
45	42, 44	sseldd 3604	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ 𝐼)
46	29	ralrimiva 2966	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
47	46	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48		sneq 4187	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑥) → {𝑖} = {(1^st ‘𝑥)})
49	48	imaeq2d 5466	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑥)}))
50		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑖𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑗))
51	49, 50	mpteq12dv 4733	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
52	51	breq2d 4665	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
53	52	rspcv 3305	. . . . . . . 8 ⊢ ((1^st ‘𝑥) ∈ 𝐼 → (∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
54	45, 47, 53	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
55	54	3ad2antr1 1226	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
56	55	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
57		ovex 6678	. . . . . . 7 ⊢ ((1^st ‘𝑥)𝑆𝑗) ∈ V
58		eqid 2622	. . . . . . 7 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
59	57, 58	dmmpti 6023	. . . . . 6 ⊢ dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)})
60	59	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)}))
61		1st2nd 7214	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
62	11, 61	sylan 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
63		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
64	62, 63	eqeltrrd 2702	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
65		df-br 4654	. . . . . . . . 9 ⊢ ((1^st ‘𝑥)𝐴(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
66	64, 65	sylibr 224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥)𝐴(2^nd ‘𝑥))
67	11	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴)
68		elrelimasn 5489	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
69	67, 68	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
70	66, 69	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
71	70	3ad2antr1 1226	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
72	71	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
73	11	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴)
74		simpr2 1068	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴)
75		1st2nd 7214	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
76	73, 74, 75	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
77	76, 74	eqeltrrd 2702	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
78		df-br 4654	. . . . . . . . 9 ⊢ ((1^st ‘𝑦)𝐴(2^nd ‘𝑦) ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
79	77, 78	sylibr 224	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦)𝐴(2^nd ‘𝑦))
80		elrelimasn 5489	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
81	73, 80	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
82	79, 81	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
83	82	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
84		simpr 477	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (1^st ‘𝑥) = (1^st ‘𝑦))
85	84	sneqd 4189	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → {(1^st ‘𝑥)} = {(1^st ‘𝑦)})
86	85	imaeq2d 5466	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝐴 “ {(1^st ‘𝑥)}) = (𝐴 “ {(1^st ‘𝑦)}))
87	83, 86	eleqtrrd 2704	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
88		simplr3 1105	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝑥 ≠ 𝑦)
89		simpr1 1067	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴)
90	73, 89, 61	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
91	90, 76	eqeq12d 2637	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
92		fvex 6201	. . . . . . . . . 10 ⊢ (1^st ‘𝑥) ∈ V
93		fvex 6201	. . . . . . . . . 10 ⊢ (2^nd ‘𝑥) ∈ V
94	92, 93	opth 4945	. . . . . . . . 9 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
95	91, 94	syl6bb 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦))))
96	95	baibd 948	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
97	96	necon3bid 2838	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2^nd ‘𝑥) ≠ (2^nd ‘𝑦)))
98	88, 97	mpbid 222	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ≠ (2^nd ‘𝑦))
99	56, 60, 72, 87, 98, 1	dprdcntz 18407	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))))
100		df-ov 6653	. . . . . 6 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
101		oveq2 6658	. . . . . . . 8 ⊢ (𝑗 = (2^nd ‘𝑥) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
102	101, 58, 57	fvmpt3i 6287	. . . . . . 7 ⊢ ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
103	71, 102	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
104	90	fveq2d 6195	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
105	100, 103, 104	3eqtr4a 2682	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
106	105	adantr 481	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
107	84	oveq1d 6665	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
108	86, 107	mpteq12dv 4733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
109	108	fveq1d 6193	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)))
110		df-ov 6653	. . . . . . . 8 ⊢ ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
111		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑦)𝑆𝑗) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
112		eqid 2622	. . . . . . . . . 10 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))
113		ovex 6678	. . . . . . . . . 10 ⊢ ((1^st ‘𝑦)𝑆𝑗) ∈ V
114	111, 112, 113	fvmpt3i 6287	. . . . . . . . 9 ⊢ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
115	82, 114	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
116	76	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
117	110, 115, 116	3eqtr4a 2682	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
118	117	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
119	109, 118	eqtrd 2656	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
120	119	fveq2d 6195	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦)))
121	99, 106, 120	3sstr3d 3647	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
122	11, 41, 12, 29, 4, 3	dprd2dlem2 18439	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
123	51	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
124	123, 17, 16	fvmpt3i 6287	. . . . . . . 8 ⊢ ((1^st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
125	45, 124	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
126	122, 125	sseqtr4d 3642	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
127	126	3ad2antr1 1226	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
128	127	adantr 481	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
129	4	ad2antrr 762	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
130	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
131	45	3ad2antr1 1226	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
132	131	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
133	12	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼)
134		1stdm 7215	. . . . . . . . 9 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → (1^st ‘𝑦) ∈ dom 𝐴)
135	73, 74, 134	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ dom 𝐴)
136	133, 135	sseldd 3604	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
137	136	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
138		simpr 477	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ≠ (1^st ‘𝑦))
139	129, 130, 132, 137, 138, 1	dprdcntz 18407	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))))
140		sneq 4187	. . . . . . . . . . . . 13 ⊢ (𝑖 = (1^st ‘𝑦) → {𝑖} = {(1^st ‘𝑦)})
141	140	imaeq2d 5466	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑦)}))
142		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑖𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
143	141, 142	mpteq12dv 4733	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
144	143	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
145	144, 17, 16	fvmpt3i 6287	. . . . . . . . 9 ⊢ ((1^st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
146	136, 145	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
147	146	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))))
148		eqid 2622	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
149	148	dprdssv 18415	. . . . . . . 8 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
150	46	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151	143	breq2d 4665	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
152	151	rspcv 3305	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑦) ∈ 𝐼 → (∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
153	136, 150, 152	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
154	113, 112	dmmpti 6023	. . . . . . . . . . 11 ⊢ dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑦)})
155	154	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑦)}))
156	153, 155, 82	dprdub 18424	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
157	117, 156	eqsstr3d 3640	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
158	148, 1	cntz2ss 17765	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
159	149, 157, 158	sylancr 695	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
160	147, 159	eqsstrd 3639	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
161	160	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
162	139, 161	sstrd 3613	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
163	128, 162	sstrd 3613	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
164	121, 163	pm2.61dane 2881	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
165	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp)
166	148	subgacs 17629	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
167		acsmre 16313	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
168	165, 166, 167	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
169	14	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴)
170		undif2 4044	. . . . . . . . . . . . . . . . . 18 ⊢ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})) = ({(1^st ‘𝑥)} ∪ 𝐼)
171	45	snssd 4340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1^st ‘𝑥)} ⊆ 𝐼)
172		ssequn1 3783	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(1^st ‘𝑥)} ⊆ 𝐼 ↔ ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
173	171, 172	sylib 208	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
174	170, 173	syl5req 2669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})))
175	174	reseq2d 5396	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
176	169, 175	eqtr3d 2658	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
177		resundi 5410	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))) = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
178	176, 177	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
179	178	difeq1d 3727	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}))
180		difundir 3880	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
181	179, 180	syl6eq 2672	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})))
182		neirr 2803	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (1^st ‘𝑥) ≠ (1^st ‘𝑥)
183	62	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
184		df-br 4654	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
185	93	brres 5402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ((1^st ‘𝑥)𝐴(2^nd ‘𝑥) ∧ (1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)})))
186	185	simprbi 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}))
187		eldifsni 4320	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
188	186, 187	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
189	184, 188	sylbir 225	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
190	183, 189	syl6bi 243	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥)))
191	182, 190	mtoi 190	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
192		disjsn 4246	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
193	191, 192	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅)
194		disj3 4021	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
195	193, 194	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
196	195	eqcomd 2628	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
197	196	uneq2d 3767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
198	181, 197	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
199	198	imaeq2d 5466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
200		imaundi 5545	. . . . . . . . . 10 ⊢ (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
201	199, 200	syl6eq 2672	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
202	201	unieqd 4446	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
203		uniun 4456	. . . . . . . 8 ⊢ ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
204	202, 203	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
205		imassrn 5477	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
206		frn 6053	. . . . . . . . . . . . . 14 ⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺))
207	41, 206	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
208	207	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
209		mresspw 16252	. . . . . . . . . . . . 13 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
210	168, 209	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
211	208, 210	sstrd 3613	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
212	205, 211	syl5ss 3614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
213		sspwuni 4611	. . . . . . . . . 10 ⊢ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
214	212, 213	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
215	168, 3, 214	mrcssidd 16285	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
216		imassrn 5477	. . . . . . . . . . 11 ⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ ran 𝑆
217	216, 211	syl5ss 3614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
218		sspwuni 4611	. . . . . . . . . 10 ⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
219	217, 218	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
220	168, 3, 219	mrcssidd 16285	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
221		unss12 3785	. . . . . . . 8 ⊢ ((∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
222	215, 220, 221	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
223	204, 222	eqsstrd 3639	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
224	3	mrccl 16271	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
225	168, 214, 224	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
226	3	mrccl 16271	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
227	168, 219, 226	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
228		eqid 2622	. . . . . . . 8 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
229	228	lsmunss 18073	. . . . . . 7 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
230	225, 227, 229	syl2anc 693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
231	223, 230	sstrd 3613	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
232		difss 3737	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1^st ‘𝑥)})
233		ressn 5671	. . . . . . . . . . . . 13 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) = ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
234	232, 233	sseqtri 3637	. . . . . . . . . . . 12 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
235		imass2 5501	. . . . . . . . . . . 12 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))))
236	234, 235	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
237		ovex 6678	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝑆𝑖) ∈ V
238		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑖))
239	58, 238	elrnmpt1s 5373	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ ((1^st ‘𝑥)𝑆𝑖) ∈ V) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
240	237, 239	mpan2 707	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
241	240	rgen 2922	. . . . . . . . . . . . . 14 ⊢ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
242	241	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
243		oveq1 6657	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (1^st ‘𝑥) → (𝑦𝑆𝑖) = ((1^st ‘𝑥)𝑆𝑖))
244	243	eleq1d 2686	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (1^st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
245	244	ralbidv 2986	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (1^st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
246	92, 245	ralsn 4222	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
247	242, 246	sylibr 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
248	41	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
249		ffun 6048	. . . . . . . . . . . . . 14 ⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆)
250	248, 249	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆)
251		resss 5422	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) ⊆ 𝐴
252	233, 251	eqsstr3i 3636	. . . . . . . . . . . . . 14 ⊢ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ 𝐴
253		fdm 6051	. . . . . . . . . . . . . . 15 ⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐴)
254	248, 253	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴)
255	252, 254	syl5sseqr 3654	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ dom 𝑆)
256		funimassov 6811	. . . . . . . . . . . . 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 ‘𝑥)𝑆𝑗))))
257	250, 255, 256	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
258	247, 257	mpbird 247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
259	236, 258	syl5ss 3614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
260	259	unissd 4462	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
261		df-ov 6653	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑥)𝑆𝑗) = (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩)
262	41	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
263		elrelimasn 5489	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
264	67, 263	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
265	264	biimpa 501	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (1^st ‘𝑥)𝐴𝑗)
266		df-br 4654	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝐴𝑗 ↔ ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
267	265, 266	sylib 208	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
268	262, 267	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
269	261, 268	syl5eqel 2705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ((1^st ‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
270	269, 58	fmptd 6385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺))
271		frn 6053	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
272	270, 271	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
273	272, 210	sstrd 3613	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
274		sspwuni 4611	. . . . . . . . . 10 ⊢ (ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
275	273, 274	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
276	168, 3, 260, 275	mrcssd 16284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
277	3	dprdspan 18426	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
278	54, 277	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
279	276, 278	sseqtr4d 3642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
280	16, 17	fnmpti 6022	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
281		fnressn 6425	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1^st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
282	280, 45, 281	sylancr 695	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
283	125	opeq2d 4409	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩ = ⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩)
284	283	sneqd 4189	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩} = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
285	282, 284	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
286	285	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}))
287		dprdsubg 18423	. . . . . . . . . . . . 13 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
288	54, 287	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
289		dprdsn 18435	. . . . . . . . . . . 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 ‘𝑥)𝑆𝑗)))))
290	45, 288, 289	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))))
291	290	simprd 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
292	286, 291	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
293	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
294	18	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
295		difss 3737	. . . . . . . . . . 11 ⊢ (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼
296	295	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼)
297		disjdif 4040	. . . . . . . . . . 11 ⊢ ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅
298	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅)
299	293, 294, 171, 296, 298, 1	dprdcntz2 18437	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
300	292, 299	eqsstr3d 3640	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
301	29	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
302	67, 248, 42, 301, 293, 3, 296	dprd2dlem1 18440	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
303		resmpt 5449	. . . . . . . . . . . 12 ⊢ ((𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
304	295, 303	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
305	304	oveq2i 6661	. . . . . . . . . 10 ⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
306	302, 305	syl6eqr 2674	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
307	306	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
308	300, 307	sseqtr4d 3642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
309	279, 308	sstrd 3613	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
310	228, 1	lsmsubg 18069	. . . . . 6 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
311	225, 227, 309, 310	syl3anc 1326	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
312	3	mrcsscl 16280	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∧ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
313	168, 231, 311, 312	syl3anc 1326	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
314		sslin 3839	. . . 4 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
315	313, 314	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
316	41	ffvelrnda 6359	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺))
317	228	lsmlub 18078	. . . . . . . . . 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 ‘𝑥)𝑆𝑗)))))
318	225, 316, 288, 317	syl3anc 1326	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))))
319	279, 122, 318	mpbi2and 956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
320	319, 125	sseqtr4d 3642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
321	293, 294, 296	dprdres 18427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
322	321	simpld 475	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
323	3	dprdspan 18426	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
324	322, 323	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
325		df-ima 5127	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
326	325	unieqi 4445	. . . . . . . . . . 11 ⊢ ∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
327	326	fveq2i 6194	. . . . . . . . . 10 ⊢ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
328	324, 327	syl6eqr 2674	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
329	306, 328	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
330		eqimss 3657	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
331	329, 330	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
332		ss2in 3840	. . . . . . 7 ⊢ ((((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))))
333	320, 331, 332	syl2anc 693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))))
334	293, 294, 45, 2, 3	dprddisj 18408	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) = {(0_g‘𝐺)})
335	333, 334	sseqtrd 3641	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ {(0_g‘𝐺)})
336	228	lsmub2 18072	. . . . . . . . 9 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
337	225, 316, 336	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
338	2	subg0cl 17602	. . . . . . . . 9 ⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
339	316, 338	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
340	337, 339	sseldd 3604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
341	2	subg0cl 17602	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
342	227, 341	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
343	340, 342	elind 3798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
344	343	snssd 4340	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
345	335, 344	eqssd 3620	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = {(0_g‘𝐺)})
346		incom 3805	. . . . 5 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
347	70, 102	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
348	62	fveq2d 6195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
349	100, 347, 348	3eqtr4a 2682	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
350		eqimss2 3658	. . . . . . . . 9 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
351	349, 350	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
352		eldifsn 4317	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥))
353	11	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴)
354		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
355	251, 354	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴)
356	353, 355, 75	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
357	356	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
358	357, 110	syl6eqr 2674	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
359	356, 354	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
360		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑦) ∈ V
361	360	opelres 5401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ↔ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴 ∧ (1^st ‘𝑦) ∈ {(1^st ‘𝑥)}))
362	361	simprbi 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
363	359, 362	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
364		elsni 4194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} → (1^st ‘𝑦) = (1^st ‘𝑥))
365	363, 364	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) = (1^st ‘𝑥))
366	365	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
367	358, 366	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
368	354, 233	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
369		xp2nd 7199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
370	368, 369	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
371		simprr 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥)
372	62	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
373	356, 372	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
374		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑦) ∈ V
375	374, 360	opth 4945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ ((1^st ‘𝑦) = (1^st ‘𝑥) ∧ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
376	375	baib 944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1^st ‘𝑦) = (1^st ‘𝑥) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
377	365, 376	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
378	373, 377	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
379	378	necon3bid 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
380	371, 379	mpbid 222	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ≠ (2^nd ‘𝑥))
381		eldifsn 4317	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↔ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
382	370, 380, 381	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
383		ovex 6678	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ V
384		difss 3737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)})
385		resmpt 5449	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
386	384, 385	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
387		oveq2 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
388	386, 387	elrnmpt1s 5373	. . . . . . . . . . . . . . . . 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 ‘𝑥)})))
389	382, 383, 388	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
390	367, 389	eqeltrd 2701	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
391		df-ima 5127	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
392	390, 391	syl6eleqr 2712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
393	392	ex 450	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
394	352, 393	syl5bi 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
395	394	ralrimiv 2965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
396	234, 255	syl5ss 3614	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
397		funimass4 6247	. . . . . . . . . . . 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 ‘𝑥)}))))
398	250, 396, 397	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
399	395, 398	mpbird 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
400	399	unissd 4462	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
401		imassrn 5477	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
402	401, 273	syl5ss 3614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺))
403		sspwuni 4611	. . . . . . . . . 10 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
404	402, 403	sylib 208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
405	168, 3, 400, 404	mrcssd 16284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
406		ss2in 3840	. . . . . . . 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 ‘𝑥)})))))
407	351, 405, 406	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))))
408	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1^st ‘𝑥)}))
409	54, 408, 70, 2, 3	dprddisj 18408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))) = {(0_g‘𝐺)})
410	407, 409	sseqtrd 3641	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
411	2	subg0cl 17602	. . . . . . . . 9 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
412	225, 411	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
413	339, 412	elind 3798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
414	413	snssd 4340	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
415	410, 414	eqssd 3620	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) = {(0_g‘𝐺)})
416	346, 415	syl5eq 2668	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0_g‘𝐺)})
417	228, 225, 316, 227, 2, 345, 416	lsmdisj2 18095	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) = {(0_g‘𝐺)})
418	315, 417	sseqtrd 3641	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
419	1, 2, 3, 6, 40, 41, 164, 418	dmdprdd 18398	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 ⟨cop 4183 ∪ cuni 4436 ∪ ciun 4520 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 dom cdm 5114 ran crn 5115 ↾ cres 5116 “ cima 5117 Rel wrel 5119 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 Basecbs 15857 0_gc0g 16100 Moorecmre 16242 mrClscmrc 16243 ACScacs 16245 Grpcgrp 17422 SubGrpcsubg 17588 Cntzccntz 17748 LSSumclsm 18049 DProd cdprd 18392

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-0g 16102 df-gsum 16103 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-submnd 17336 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-ghm 17658 df-gim 17701 df-cntz 17750 df-oppg 17776 df-lsm 18051 df-cmn 18195 df-dprd 18394

This theorem is referenced by: dprd2db 18442 dprd2d2 18443

W3C validator