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 20177

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 2762	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2762	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		dprd2d.k	. 2 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))
4		dprd2d.5	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5		dprdgrp 20140	. . 3 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
6	4, 5	syl 18	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		resiun2 5997	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖})
8		iunid 5023	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼
9	8	reseq2i 5973	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼)
10	7, 9	eqtr3i 2787	. . . 4 ⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼)
11		dprd2d.1	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
12		dprd2d.3	. . . . 5 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)
13		relssres 6019	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴)
14	11, 12, 13	syl2anc 596	. . . 4 ⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴)
15	10, 14	eqtrid 2809	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16		ovex 7450	. . . . . 6 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17		eqid 2762	. . . . . 6 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
18	16, 17	dmmpti 6680	. . . . 5 ⊢ dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19		reldmdprd 20132	. . . . . . 7 ⊢ Rel dom DProd
20	19	brrelex2i 5716	. . . . . 6 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21		dmexg 7902	. . . . . 6 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
22	4, 20, 21	3syl 19	. . . . 5 ⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
23	18, 22	eqeltrrid 2867	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
24		ressn 6287	. . . . . 6 ⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25		vsnex 5404	. . . . . . 7 ⊢ {𝑖} ∈ V
26		ovex 7450	. . . . . . . . 9 ⊢ (𝑖𝑆𝑗) ∈ V
27		eqid 2762	. . . . . . . . 9 ⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
28	26, 27	dmmpti 6680	. . . . . . . 8 ⊢ dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29		dprd2d.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30	19	brrelex2i 5716	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31		dmexg 7902	. . . . . . . . 9 ⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
32	29, 30, 31	3syl 19	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
33	28, 32	eqeltrrid 2867	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V)
34		xpexg 7753	. . . . . . 7 ⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
35	25, 33, 34	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
36	24, 35	eqeltrid 2866	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
37	36	ralrimiva 3156	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38		iunexg 7964	. . . 4 ⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
39	23, 37, 38	syl2anc 596	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
40	15, 39	eqeltrrd 2863	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
41		dprd2d.2	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
42		sneq 4597	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → {𝑖} = {(1^st ‘𝑥)})
43	42	imaeq2d 6060	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑥)}))
44		oveq1 7424	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑖𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑗))
45	43, 44	mpteq12dv 5196	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
46	45	breq2d 5119	. . . . . . . 8 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
47	29	ralrimiva 3156	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48	47	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
49	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼)
50		1stdm 8041	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
51	11, 50	sylan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
52	49, 51	sseldd 3935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ 𝐼)
53	46, 48, 52	rspcdva 3580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
54	53	3ad2antr1 1207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
55	54	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
56		ovex 7450	. . . . . . 7 ⊢ ((1^st ‘𝑥)𝑆𝑗) ∈ V
57		eqid 2762	. . . . . . 7 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
58	56, 57	dmmpti 6680	. . . . . 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 8040	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
61	11, 60	sylan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
62		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
63	61, 62	eqeltrrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
64		df-br 5108	. . . . . . . . 9 ⊢ ((1^st ‘𝑥)𝐴(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
65	63, 64	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥)𝐴(2^nd ‘𝑥))
66	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴)
67		elrelimasn 6086	. . . . . . . . 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 486	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
72	11	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴)
73		simpr2 1214	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴)
74		1st2nd 8040	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
75	72, 73, 74	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
76	75, 73	eqeltrrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
77		df-br 5108	. . . . . . . . 9 ⊢ ((1^st ‘𝑦)𝐴(2^nd ‘𝑦) ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
78	76, 77	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦)𝐴(2^nd ‘𝑦))
79		elrelimasn 6086	. . . . . . . . 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 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
83		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (1^st ‘𝑥) = (1^st ‘𝑦))
84	83	sneqd 4599	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → {(1^st ‘𝑥)} = {(1^st ‘𝑦)})
85	84	imaeq2d 6060	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝐴 “ {(1^st ‘𝑥)}) = (𝐴 “ {(1^st ‘𝑦)}))
86	82, 85	eleqtrrd 2865	. . . . 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 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
90	89, 75	eqeq12d 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
91		fvex 6895	. . . . . . . . . 10 ⊢ (1^st ‘𝑥) ∈ V
92		fvex 6895	. . . . . . . . . 10 ⊢ (2^nd ‘𝑥) ∈ V
93	91, 92	opth 5456	. . . . . . . . 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 549	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
96	95	necon3bid 3001	. . . . . 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 20143	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))))
99		df-ov 7420	. . . . . 6 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
100		oveq2 7425	. . . . . . . 8 ⊢ (𝑗 = (2^nd ‘𝑥) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
101	100, 57, 56	fvmpt3i 6996	. . . . . . 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 6886	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
104	99, 102, 103	3eqtr4a 2823	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
105	104	adantr 486	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
106	83	oveq1d 7432	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
107	85, 106	mpteq12dv 5196	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
108	107	fveq1d 6884	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)))
109		df-ov 7420	. . . . . . . 8 ⊢ ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
110		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑦)𝑆𝑗) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
111		eqid 2762	. . . . . . . . . 10 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))
112		ovex 7450	. . . . . . . . . 10 ⊢ ((1^st ‘𝑦)𝑆𝑗) ∈ V
113	110, 111, 112	fvmpt3i 6996	. . . . . . . . 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 6886	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
116	109, 114, 115	3eqtr4a 2823	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
117	116	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
118	108, 117	eqtrd 2797	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
119	118	fveq2d 6886	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦)))
120	98, 105, 119	3sstr3d 3988	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
121	11, 41, 12, 29, 4, 3	dprd2dlem2 20175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
122	45	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
123	122, 17, 16	fvmpt3i 6996	. . . . . . . 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 3971	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
126	125	3ad2antr1 1207	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
127	126	adantr 486	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
128	4	ad2antrr 739	. . . . . 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 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
132	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼)
133		1stdm 8041	. . . . . . . . 9 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → (1^st ‘𝑦) ∈ dom 𝐴)
134	72, 73, 133	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ dom 𝐴)
135	132, 134	sseldd 3935	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
136	135	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
137		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ≠ (1^st ‘𝑦))
138	128, 129, 131, 136, 137, 1	dprdcntz 20143	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))))
139		sneq 4597	. . . . . . . . . . . . 13 ⊢ (𝑖 = (1^st ‘𝑦) → {𝑖} = {(1^st ‘𝑦)})
140	139	imaeq2d 6060	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑦)}))
141		oveq1 7424	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑖𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
142	140, 141	mpteq12dv 5196	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
143	142	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
144	143, 17, 16	fvmpt3i 6996	. . . . . . . . 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 6886	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))))
147		eqid 2762	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
148	147	dprdssv 20151	. . . . . . . 8 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149	142	breq2d 5119	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
150	47	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151	149, 150, 135	rspcdva 3580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
152	112, 111	dmmpti 6680	. . . . . . . . . . 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 20160	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
155	116, 154	eqsstrrd 3969	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
156	147, 1	cntz2ss 19468	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
157	148, 155, 156	sylancr 599	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
158	146, 157	eqsstrd 3968	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
159	158	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
160	138, 159	sstrd 3944	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
161	127, 160	sstrd 3944	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
162	120, 161	pm2.61dane 3044	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
163	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp)
164	147	subgacs 19290	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165		acsmre 17746	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166	163, 164, 165	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
167	14	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴)
168		undif2 4434	. . . . . . . . . . . . . . . . . 18 ⊢ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})) = ({(1^st ‘𝑥)} ∪ 𝐼)
169	52	snssd 4750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1^st ‘𝑥)} ⊆ 𝐼)
170		ssequn1 4135	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(1^st ‘𝑥)} ⊆ 𝐼 ↔ ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
171	169, 170	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
172	168, 171	eqtr2id 2810	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})))
173	172	reseq2d 5976	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
174	167, 173	eqtr3d 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
175		resundi 5990	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))) = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
176	174, 175	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
177	176	difeq1d 4076	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}))
178		difundir 4240	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
179	177, 178	eqtrdi 2813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})))
180		neirr 2966	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (1^st ‘𝑥) ≠ (1^st ‘𝑥)
181	61	eleq1d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
182		df-br 5108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
183	92	brresi 5985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ∧ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
184	183	simplbi 502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}))
185		eldifsni 4756	. . . . . . . . . . . . . . . . . . . 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 4675	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
191	189, 190	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅)
192		disj3 4410	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
193	191, 192	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
194	193	eqcomd 2768	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
195	194	uneq2d 4118	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
196	179, 195	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
197	196	imaeq2d 6060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
198		imaundi 6145	. . . . . . . . . 10 ⊢ (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
199	197, 198	eqtrdi 2813	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
200	199	unieqd 4883	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
201		uniun 4893	. . . . . . . 8 ⊢ ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
202	200, 201	eqtrdi 2813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
203		imassrn 6071	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
204	41	frnd 6715	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205	204	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206		mresspw 17682	. . . . . . . . . . . . 13 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207	166, 206	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208	205, 207	sstrd 3944	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209	203, 208	sstrid 3945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210		sspwuni 5064	. . . . . . . . . 10 ⊢ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211	209, 210	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212	166, 3, 211	mrcssidd 17719	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
213		imassrn 6071	. . . . . . . . . . 11 ⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ ran 𝑆
214	213, 208	sstrid 3945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215		sspwuni 5064	. . . . . . . . . 10 ⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
216	214, 215	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
217	166, 3, 216	mrcssidd 17719	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
218		unss12 4137	. . . . . . . 8 ⊢ ((∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
219	212, 217, 218	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
220	202, 219	eqsstrd 3968	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
221	3	mrccl 17705	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222	166, 211, 221	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
223	3	mrccl 17705	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
224	166, 216, 223	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
225		eqid 2762	. . . . . . . 8 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
226	225	lsmunss 19792	. . . . . . 7 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
227	222, 224, 226	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
228	220, 227	sstrd 3944	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
229		difss 4086	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1^st ‘𝑥)})
230		ressn 6287	. . . . . . . . . . . . 13 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) = ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
231	229, 230	sseqtri 3982	. . . . . . . . . . . 12 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
232		imass2 6102	. . . . . . . . . . . 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 7450	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝑆𝑖) ∈ V
235		oveq2 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑖))
236	57, 235	elrnmpt1s 5947	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ ((1^st ‘𝑥)𝑆𝑖) ∈ V) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
237	234, 236	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
238	237	rgen 3080	. . . . . . . . . . . . . 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 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (1^st ‘𝑥) → (𝑦𝑆𝑖) = ((1^st ‘𝑥)𝑆𝑖))
241	240	eleq1d 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (1^st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
242	241	ralbidv 3187	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (1^st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
243	91, 242	ralsn 4645	. . . . . . . . . . . . 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 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
246	245	ffund 6711	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆)
247		resss 5998	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) ⊆ 𝐴
248	230, 247	eqsstrri 3981	. . . . . . . . . . . . . 14 ⊢ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ 𝐴
249	245	fdmd 6717	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴)
250	248, 249	sseqtrrid 3977	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ dom 𝑆)
251		funimassov 7595	. . . . . . . . . . . . 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 596	. . . . . . . . . . . 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 3945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
255	254	unissd 4880	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
256		df-ov 7420	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑥)𝑆𝑗) = (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩)
257	41	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258		elrelimasn 6086	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
259	66, 258	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
260	259	biimpa 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (1^st ‘𝑥)𝐴𝑗)
261		df-br 5108	. . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ((1^st ‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265	264	fmpttd 7112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺))
266	265	frnd 6715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267	266, 207	sstrd 3944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268		sspwuni 5064	. . . . . . . . . 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 17718	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
271	3	dprdspan 20162	. . . . . . . . 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 3971	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
274	16, 17	fnmpti 6679	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275		fnressn 7159	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1^st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
276	274, 52, 275	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
277	124	opeq2d 4843	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩ = ⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩)
278	277	sneqd 4599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩} = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
279	276, 278	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
280	279	oveq2d 7433	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}))
281		dprdsubg 20159	. . . . . . . . . . . . 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 20171	. . . . . . . . . . . 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 596	. . . . . . . . . . 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 501	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
286	280, 285	eqtrd 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
287	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
288	18	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
289		difss 4086	. . . . . . . . . . 11 ⊢ (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼
290	289	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼)
291		disjdif 4429	. . . . . . . . . . 11 ⊢ ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅
292	291	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅)
293	287, 288, 169, 290, 292, 1	dprdcntz2 20173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
294	286, 293	eqsstrrd 3969	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
295	29	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
296	66, 245, 49, 295, 287, 3, 290	dprd2dlem1 20176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297		resmpt 6037	. . . . . . . . . . . 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 7428	. . . . . . . . . 10 ⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300	296, 299	eqtr4di 2815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
301	300	fveq2d 6886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
302	294, 301	sseqtrrd 3971	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
303	273, 302	sstrd 3944	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
304	225, 1	lsmsubg 19787	. . . . . 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 17714	. . . . 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 4191	. . . 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 19797	. . . . . . . . . 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 725	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
314	313, 124	sseqtrrd 3971	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
315	287, 288, 290	dprdres 20163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
316	315	simpld 500	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
317	3	dprdspan 20162	. . . . . . . . . . 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 5672	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
320	319	unieqi 4882	. . . . . . . . . . 11 ⊢ ∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
321	320	fveq2i 6885	. . . . . . . . . 10 ⊢ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
322	318, 321	eqtr4di 2815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
323	300, 322	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
324		eqimss 3992	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
325	323, 324	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
326		ss2in 4193	. . . . . . 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 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))))
328	287, 288, 52, 2, 3	dprddisj 20144	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) = {(0_g‘𝐺)})
329	327, 328	sseqtrd 3970	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ {(0_g‘𝐺)})
330	225	lsmub2 19791	. . . . . . . . 9 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
331	222, 310, 330	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
332	2	subg0cl 19263	. . . . . . . . 9 ⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
333	310, 332	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
334	331, 333	sseldd 3935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
335	2	subg0cl 19263	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
336	224, 335	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
337	334, 336	elind 4149	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
338	337	snssd 4750	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
339	329, 338	eqssd 3951	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = {(0_g‘𝐺)})
340		incom 4158	. . . . 5 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
341	69, 101	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
342	61	fveq2d 6886	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
343	99, 341, 342	3eqtr4a 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
344		eqimss2 3993	. . . . . . . . 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 4751	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥))
347	11	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴)
348		simprl 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
349	247, 348	sselid 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴)
350	347, 349, 74	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
351	350	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
352	351, 109	eqtr4di 2815	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
353	350, 348	eqeltrrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
354		fvex 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑦) ∈ V
355	354	opelresi 5984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ↔ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} ∧ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴))
356	355	simplbi 502	. . . . . . . . . . . . . . . . . . . 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 4604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} → (1^st ‘𝑦) = (1^st ‘𝑥))
359	357, 358	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) = (1^st ‘𝑥))
360	359	oveq1d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
361	352, 360	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
362	348, 230	eleqtrdi 2872	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
363		xp2nd 8023	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
364	362, 363	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
365		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥)
366	61	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
367	350, 366	eqeq12d 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
368		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑦) ∈ V
369	368, 354	opth 5456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ ((1^st ‘𝑦) = (1^st ‘𝑥) ∧ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
370	369	baib 545	. . . . . . . . . . . . . . . . . . . . . 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 3001	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
374	365, 373	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ≠ (2^nd ‘𝑥))
375		eldifsn 4751	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↔ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
376	364, 374, 375	sylanbrc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
377		ovex 7450	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ V
378		difss 4086	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)})
379		resmpt 6037	. . . . . . . . . . . . . . . . . . 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 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
382	380, 381	elrnmpt1s 5947	. . . . . . . . . . . . . . . . 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 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
384	361, 383	eqeltrd 2862	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
385		df-ima 5672	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
386	384, 385	eleqtrrdi 2873	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
387	386	ex 418	. . . . . . . . . . . . 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 3155	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
390	231, 250	sstrid 3945	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391		funimass4 6946	. . . . . . . . . . . 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 596	. . . . . . . . . . 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 4880	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
395		imassrn 6071	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
396	395, 267	sstrid 3945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397		sspwuni 5064	. . . . . . . . . 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 17718	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
400		ss2in 4193	. . . . . . . 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 596	. . . . . . 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 20144	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))) = {(0_g‘𝐺)})
404	401, 403	sseqtrd 3970	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
405	2	subg0cl 19263	. . . . . . . . 9 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
406	222, 405	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
407	333, 406	elind 4149	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
408	407	snssd 4750	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
409	404, 408	eqssd 3951	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) = {(0_g‘𝐺)})
410	340, 409	eqtrid 2809	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0_g‘𝐺)})
411	225, 222, 310, 224, 2, 339, 410	lsmdisj2 19815	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) = {(0_g‘𝐺)})
412	309, 411	sseqtrd 3970	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
413	1, 2, 3, 6, 40, 41, 162, 412	dmdprdd 20134	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 𝒫 cpw 4560 {csn 4587 ⟨cop 4593 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 Rel wrel 5664 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 1^st c1st 7988 2^nd c2nd 7989 Basecbs 17307 0_gc0g 17530 Moorecmre 17672 mrClscmrc 17673 ACScacs 17675 Grpcgrp 19063 SubGrpcsubg 19249 Cntzccntz 19448 LSSumclsm 19767 DProd cdprd 20128

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-n0 12533 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-seq 14070 df-hash 14399 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-0g 17532 df-gsum 17533 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-gim 19392 df-cntz 19450 df-oppg 19479 df-lsm 19769 df-cmn 19915 df-dprd 20130

This theorem is used by: dprd2db 20178 dprd2d2 20179

W3C validator