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 19958

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 2733	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2733	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		dprd2d.k	. 2 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))
4		dprd2d.5	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5		dprdgrp 19921	. . 3 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		resiun2 5953	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖})
8		iunid 5011	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼
9	8	reseq2i 5929	. . . . 5 ⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼)
10	7, 9	eqtr3i 2758	. . . 4 ⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼)
11		dprd2d.1	. . . . 5 ⊢ (𝜑 → Rel 𝐴)
12		dprd2d.3	. . . . 5 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼)
13		relssres 5975	. . . . 5 ⊢ ((Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴)
14	11, 12, 13	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴)
15	10, 14	eqtrid 2780	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16		ovex 7385	. . . . . 6 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17		eqid 2733	. . . . . 6 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
18	16, 17	dmmpti 6630	. . . . 5 ⊢ dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19		reldmdprd 19913	. . . . . . 7 ⊢ Rel dom DProd
20	19	brrelex2i 5676	. . . . . 6 ⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21		dmexg 7837	. . . . . 6 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
22	4, 20, 21	3syl 18	. . . . 5 ⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
23	18, 22	eqeltrrid 2838	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
24		ressn 6237	. . . . . 6 ⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25		vsnex 5374	. . . . . . 7 ⊢ {𝑖} ∈ V
26		ovex 7385	. . . . . . . . 9 ⊢ (𝑖𝑆𝑗) ∈ V
27		eqid 2733	. . . . . . . . 9 ⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
28	26, 27	dmmpti 6630	. . . . . . . 8 ⊢ dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29		dprd2d.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30	19	brrelex2i 5676	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31		dmexg 7837	. . . . . . . . 9 ⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
32	29, 30, 31	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
33	28, 32	eqeltrrid 2838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V)
34		xpexg 7689	. . . . . . 7 ⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
35	25, 33, 34	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
36	24, 35	eqeltrid 2837	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
37	36	ralrimiva 3125	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38		iunexg 7901	. . . 4 ⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
39	23, 37, 38	syl2anc 584	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V)
40	15, 39	eqeltrrd 2834	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
41		dprd2d.2	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
42		sneq 4585	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑥) → {𝑖} = {(1^st ‘𝑥)})
43	42	imaeq2d 6013	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑥)}))
44		oveq1 7359	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑖𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑗))
45	43, 44	mpteq12dv 5180	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
46	45	breq2d 5105	. . . . . . . 8 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
47	29	ralrimiva 3125	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48	47	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
49	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼)
50		1stdm 7978	. . . . . . . . . 10 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
51	11, 50	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ dom 𝐴)
52	49, 51	sseldd 3931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥) ∈ 𝐼)
53	46, 48, 52	rspcdva 3574	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
54	53	3ad2antr1 1189	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
55	54	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
56		ovex 7385	. . . . . . 7 ⊢ ((1^st ‘𝑥)𝑆𝑗) ∈ V
57		eqid 2733	. . . . . . 7 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
58	56, 57	dmmpti 6630	. . . . . 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 7977	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
61	11, 60	sylan 580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
62		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
63	61, 62	eqeltrrd 2834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
64		df-br 5094	. . . . . . . . 9 ⊢ ((1^st ‘𝑥)𝐴(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ 𝐴)
65	63, 64	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1^st ‘𝑥)𝐴(2^nd ‘𝑥))
66	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴)
67		elrelimasn 6039	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
68	66, 67	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
69	65, 68	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
70	69	3ad2antr1 1189	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
71	70	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}))
72	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴)
73		simpr2 1196	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴)
74		1st2nd 7977	. . . . . . . . . . 11 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
75	72, 73, 74	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
76	75, 73	eqeltrrd 2834	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
77		df-br 5094	. . . . . . . . 9 ⊢ ((1^st ‘𝑦)𝐴(2^nd ‘𝑦) ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴)
78	76, 77	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦)𝐴(2^nd ‘𝑦))
79		elrelimasn 6039	. . . . . . . . 9 ⊢ (Rel 𝐴 → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
80	72, 79	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) ↔ (1^st ‘𝑦)𝐴(2^nd ‘𝑦)))
81	78, 80	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
82	81	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}))
83		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (1^st ‘𝑥) = (1^st ‘𝑦))
84	83	sneqd 4587	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → {(1^st ‘𝑥)} = {(1^st ‘𝑦)})
85	84	imaeq2d 6013	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝐴 “ {(1^st ‘𝑥)}) = (𝐴 “ {(1^st ‘𝑦)}))
86	82, 85	eleqtrrd 2836	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
87		simplr3 1218	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → 𝑥 ≠ 𝑦)
88		simpr1 1195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴)
89	72, 88, 60	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
90	89, 75	eqeq12d 2749	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
91		fvex 6841	. . . . . . . . . 10 ⊢ (1^st ‘𝑥) ∈ V
92		fvex 6841	. . . . . . . . . 10 ⊢ (2^nd ‘𝑥) ∈ V
93	91, 92	opth 5419	. . . . . . . . 9 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
94	90, 93	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) = (2^nd ‘𝑦))))
95	94	baibd 539	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2^nd ‘𝑥) = (2^nd ‘𝑦)))
96	95	necon3bid 2973	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2^nd ‘𝑥) ≠ (2^nd ‘𝑦)))
97	87, 96	mpbid 232	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (2^nd ‘𝑥) ≠ (2^nd ‘𝑦))
98	55, 59, 71, 86, 97, 1	dprdcntz 19924	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))))
99		df-ov 7355	. . . . . 6 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
100		oveq2 7360	. . . . . . . 8 ⊢ (𝑗 = (2^nd ‘𝑥) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
101	100, 57, 56	fvmpt3i 6940	. . . . . . 7 ⊢ ((2^nd ‘𝑥) ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
102	70, 101	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
103	89	fveq2d 6832	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
104	99, 102, 103	3eqtr4a 2794	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
105	104	adantr 480	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
106	83	oveq1d 7367	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
107	85, 106	mpteq12dv 5180	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
108	107	fveq1d 6830	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)))
109		df-ov 7355	. . . . . . . 8 ⊢ ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
110		oveq2 7360	. . . . . . . . . 10 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑦)𝑆𝑗) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
111		eqid 2733	. . . . . . . . . 10 ⊢ (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))
112		ovex 7385	. . . . . . . . . 10 ⊢ ((1^st ‘𝑦)𝑆𝑗) ∈ V
113	110, 111, 112	fvmpt3i 6940	. . . . . . . . 9 ⊢ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
114	81, 113	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
115	75	fveq2d 6832	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
116	109, 114, 115	3eqtr4a 2794	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
117	116	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
118	108, 117	eqtrd 2768	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦)) = (𝑆‘𝑦))
119	118	fveq2d 6832	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦)))
120	98, 105, 119	3sstr3d 3985	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) = (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
121	11, 41, 12, 29, 4, 3	dprd2dlem2 19956	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
122	45	oveq2d 7368	. . . . . . . . 9 ⊢ (𝑖 = (1^st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
123	122, 17, 16	fvmpt3i 6940	. . . . . . . 8 ⊢ ((1^st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
124	52, 123	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
125	121, 124	sseqtrrd 3968	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
126	125	3ad2antr1 1189	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
127	126	adantr 480	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
128	4	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
129	18	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
130	52	3ad2antr1 1189	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
131	130	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ∈ 𝐼)
132	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼)
133		1stdm 7978	. . . . . . . . 9 ⊢ ((Rel 𝐴 ∧ 𝑦 ∈ 𝐴) → (1^st ‘𝑦) ∈ dom 𝐴)
134	72, 73, 133	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ dom 𝐴)
135	132, 134	sseldd 3931	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
136	135	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑦) ∈ 𝐼)
137		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (1^st ‘𝑥) ≠ (1^st ‘𝑦))
138	128, 129, 131, 136, 137, 1	dprdcntz 19924	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))))
139		sneq 4585	. . . . . . . . . . . . 13 ⊢ (𝑖 = (1^st ‘𝑦) → {𝑖} = {(1^st ‘𝑦)})
140	139	imaeq2d 6013	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1^st ‘𝑦)}))
141		oveq1 7359	. . . . . . . . . . . 12 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑖𝑆𝑗) = ((1^st ‘𝑦)𝑆𝑗))
142	140, 141	mpteq12dv 5180	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
143	142	oveq2d 7368	. . . . . . . . . 10 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
144	143, 17, 16	fvmpt3i 6940	. . . . . . . . 9 ⊢ ((1^st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
145	135, 144	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
146	145	fveq2d 6832	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))))
147		eqid 2733	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
148	147	dprdssv 19932	. . . . . . . 8 ⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149	142	breq2d 5105	. . . . . . . . . . 11 ⊢ (𝑖 = (1^st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
150	47	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151	149, 150, 135	rspcdva 3574	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))
152	112, 111	dmmpti 6630	. . . . . . . . . . 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 19941	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))‘(2^nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
155	116, 154	eqsstrrd 3966	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))))
156	147, 1	cntz2ss 19249	. . . . . . . 8 ⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
157	148, 155, 156	sylancr 587	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑦)}) ↦ ((1^st ‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
158	146, 157	eqsstrd 3965	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
159	158	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
160	138, 159	sstrd 3941	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
161	127, 160	sstrd 3941	. . 3 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1^st ‘𝑥) ≠ (1^st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
162	120, 161	pm2.61dane 3016	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)))
163	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp)
164	147	subgacs 19075	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165		acsmre 17560	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166	163, 164, 165	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
167	14	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴)
168		undif2 4426	. . . . . . . . . . . . . . . . . 18 ⊢ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})) = ({(1^st ‘𝑥)} ∪ 𝐼)
169	52	snssd 4760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1^st ‘𝑥)} ⊆ 𝐼)
170		ssequn1 4135	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(1^st ‘𝑥)} ⊆ 𝐼 ↔ ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
171	169, 170	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∪ 𝐼) = 𝐼)
172	168, 171	eqtr2id 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)})))
173	172	reseq2d 5932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
174	167, 173	eqtr3d 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))))
175		resundi 5946	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ ({(1^st ‘𝑥)} ∪ (𝐼 ∖ {(1^st ‘𝑥)}))) = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
176	174, 175	eqtrdi 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
177	176	difeq1d 4074	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}))
178		difundir 4240	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↾ {(1^st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
179	177, 178	eqtrdi 2784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})))
180		neirr 2938	. . . . . . . . . . . . . . . . 17 ⊢ ¬ (1^st ‘𝑥) ≠ (1^st ‘𝑥)
181	61	eleq1d 2818	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
182		df-br 5094	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
183	92	brresi 5941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) ↔ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ∧ (1^st ‘𝑥)𝐴(2^nd ‘𝑥)))
184	183	simplbi 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}))
185		eldifsni 4741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑥) ∈ (𝐼 ∖ {(1^st ‘𝑥)}) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
186	184, 185	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))(2^nd ‘𝑥) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
187	182, 186	sylbir 235	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥))
188	181, 187	biimtrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (1^st ‘𝑥) ≠ (1^st ‘𝑥)))
189	180, 188	mtoi 199	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
190		disjsn 4663	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
191	189, 190	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅)
192		disj3 4403	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
193	191, 192	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}))
194	193	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
195	194	uneq2d 4117	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
196	179, 195	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
197	196	imaeq2d 6013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
198		imaundi 6101	. . . . . . . . . 10 ⊢ (𝑆 “ (((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
199	197, 198	eqtrdi 2784	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
200	199	unieqd 4871	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
201		uniun 4881	. . . . . . . 8 ⊢ ∪ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
202	200, 201	eqtrdi 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
203		imassrn 6024	. . . . . . . . . . 11 ⊢ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
204	41	frnd 6664	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205	204	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206		mresspw 17496	. . . . . . . . . . . . 13 ⊢ ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207	166, 206	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208	205, 207	sstrd 3941	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209	203, 208	sstrid 3942	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210		sspwuni 5050	. . . . . . . . . 10 ⊢ ((𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211	209, 210	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212	166, 3, 211	mrcssidd 17533	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
213		imassrn 6024	. . . . . . . . . . 11 ⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ ran 𝑆
214	213, 208	sstrid 3942	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215		sspwuni 5050	. . . . . . . . . 10 ⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
216	214, 215	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺))
217	166, 3, 216	mrcssidd 17533	. . . . . . . 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 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
220	202, 219	eqsstrd 3965	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
221	3	mrccl 17519	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222	166, 211, 221	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
223	3	mrccl 17519	. . . . . . . 8 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
224	166, 216, 223	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺))
225		eqid 2733	. . . . . . . 8 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
226	225	lsmunss 19573	. . . . . . 7 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
227	222, 224, 226	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
228	220, 227	sstrd 3941	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
229		difss 4085	. . . . . . . . . . . . 13 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1^st ‘𝑥)})
230		ressn 6237	. . . . . . . . . . . . 13 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) = ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
231	229, 230	sseqtri 3979	. . . . . . . . . . . 12 ⊢ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))
232		imass2 6055	. . . . . . . . . . . 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 7385	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝑆𝑖) ∈ V
235		oveq2 7360	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆𝑖))
236	57, 235	elrnmpt1s 5903	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ ((1^st ‘𝑥)𝑆𝑖) ∈ V) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
237	234, 236	mpan2 691	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)}) → ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
238	237	rgen 3050	. . . . . . . . . . . . . 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 7359	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (1^st ‘𝑥) → (𝑦𝑆𝑖) = ((1^st ‘𝑥)𝑆𝑖))
241	240	eleq1d 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (1^st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
242	241	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (1^st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
243	91, 242	ralsn 4633	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})((1^st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
244	239, 243	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
245	41	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
246	245	ffund 6660	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆)
247		resss 5954	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ↾ {(1^st ‘𝑥)}) ⊆ 𝐴
248	230, 247	eqsstrri 3978	. . . . . . . . . . . . . 14 ⊢ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ 𝐴
249	245	fdmd 6666	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴)
250	248, 249	sseqtrrid 3974	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) ⊆ dom 𝑆)
251		funimassov 7529	. . . . . . . . . . . . 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 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1^st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1^st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
253	244, 252	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
254	233, 253	sstrid 3942	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
255	254	unissd 4868	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))
256		df-ov 7355	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑥)𝑆𝑗) = (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩)
257	41	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258		elrelimasn 6039	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
259	66, 258	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↔ (1^st ‘𝑥)𝐴𝑗))
260	259	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (1^st ‘𝑥)𝐴𝑗)
261		df-br 5094	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑥)𝐴𝑗 ↔ ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
262	260, 261	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ⟨(1^st ‘𝑥), 𝑗⟩ ∈ 𝐴)
263	257, 262	ffvelcdmd 7024	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → (𝑆‘⟨(1^st ‘𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
264	256, 263	eqeltrid 2837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)})) → ((1^st ‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265	264	fmpttd 7054	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)):(𝐴 “ {(1^st ‘𝑥)})⟶(SubGrp‘𝐺))
266	265	frnd 6664	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267	266, 207	sstrd 3941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268		sspwuni 5050	. . . . . . . . . 10 ⊢ (ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
269	267, 268	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
270	166, 3, 255, 269	mrcssd 17532	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
271	3	dprdspan 19943	. . . . . . . . 9 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
272	53, 271	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
273	270, 272	sseqtrrd 3968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
274	16, 17	fnmpti 6629	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275		fnressn 7097	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1^st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
276	274, 52, 275	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩})
277	124	opeq2d 4831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩ = ⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩)
278	277	sneqd 4587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {⟨(1^st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥))⟩} = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
279	276, 278	eqtrd 2768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)}) = {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩})
280	279	oveq2d 7368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}))
281		dprdsubg 19940	. . . . . . . . . . . . 13 ⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
282	53, 281	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
283		dprdsn 19952	. . . . . . . . . . . 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 584	. . . . . . . . . . 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 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {⟨(1^st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
286	280, 285	eqtrd 2768	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
287	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
288	18	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
289		difss 4085	. . . . . . . . . . 11 ⊢ (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼
290	289	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1^st ‘𝑥)}) ⊆ 𝐼)
291		disjdif 4421	. . . . . . . . . . 11 ⊢ ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅
292	291	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1^st ‘𝑥)} ∩ (𝐼 ∖ {(1^st ‘𝑥)})) = ∅)
293	287, 288, 169, 290, 292, 1	dprdcntz2 19954	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1^st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
294	286, 293	eqsstrrd 3966	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
295	29	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
296	66, 245, 49, 295, 287, 3, 290	dprd2dlem1 19957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297		resmpt 5990	. . . . . . . . . . . 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 7363	. . . . . . . . . 10 ⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1^st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300	296, 299	eqtr4di 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
301	300	fveq2d 6832	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
302	294, 301	sseqtrrd 3968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
303	273, 302	sstrd 3941	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
304	225, 1	lsmsubg 19568	. . . . . 6 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
305	222, 224, 303, 304	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ∈ (SubGrp‘𝐺))
306	3	mrcsscl 17528	. . . . 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 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
308		sslin 4192	. . . 4 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
309	307, 308	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))))
310	41	ffvelcdmda 7023	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺))
311	225	lsmlub 19578	. . . . . . . . . 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 1373	. . . . . . . . 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 712	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))))
314	313, 124	sseqtrrd 3968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)))
315	287, 288, 290	dprdres 19944	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
316	315	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
317	3	dprdspan 19943	. . . . . . . . . . 11 ⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
318	316, 317	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))
319		df-ima 5632	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
320	319	unieqi 4870	. . . . . . . . . . 11 ⊢ ∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))
321	320	fveq2i 6831	. . . . . . . . . 10 ⊢ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)})))
322	318, 321	eqtr4di 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1^st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
323	300, 322	eqtrd 2768	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
324		eqimss 3989	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
325	323, 324	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)}))))
326		ss2in 4194	. . . . . . 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 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))))
328	287, 288, 52, 2, 3	dprddisj 19925	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1^st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1^st ‘𝑥)})))) = {(0_g‘𝐺)})
329	327, 328	sseqtrd 3967	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) ⊆ {(0_g‘𝐺)})
330	225	lsmub2 19572	. . . . . . . . 9 ⊢ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
331	222, 310, 330	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
332	2	subg0cl 19049	. . . . . . . . 9 ⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
333	310, 332	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝑆‘𝑥))
334	331, 333	sseldd 3931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)))
335	2	subg0cl 19049	. . . . . . . 8 ⊢ ((𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
336	224, 335	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))
337	334, 336	elind 4149	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
338	337	snssd 4760	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))))
339	329, 338	eqssd 3948	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)}))))) = {(0_g‘𝐺)})
340		incom 4158	. . . . 5 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
341	69, 101	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑥)))
342	61	fveq2d 6832	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
343	99, 341, 342	3eqtr4a 2794	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥))
344		eqimss2 3990	. . . . . . . . 9 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
345	343, 344	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)))
346		eldifsn 4737	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥))
347	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴)
348		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
349	247, 348	sselid 3928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴)
350	347, 349, 74	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
351	350	fveq2d 6832	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
352	351, 109	eqtr4di 2786	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)))
353	350, 348	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}))
354		fvex 6841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑦) ∈ V
355	354	opelresi 5940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ↔ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} ∧ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ 𝐴))
356	355	simplbi 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝐴 ↾ {(1^st ‘𝑥)}) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
357	353, 356	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) ∈ {(1^st ‘𝑥)})
358		elsni 4592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑦) ∈ {(1^st ‘𝑥)} → (1^st ‘𝑦) = (1^st ‘𝑥))
359	357, 358	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1^st ‘𝑦) = (1^st ‘𝑥))
360	359	oveq1d 7367	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑦)𝑆(2^nd ‘𝑦)) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
361	352, 360	eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
362	348, 230	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})))
363		xp2nd 7960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ({(1^st ‘𝑥)} × (𝐴 “ {(1^st ‘𝑥)})) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
364	362, 363	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}))
365		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥)
366	61	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
367	350, 366	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
368		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑦) ∈ V
369	368, 354	opth 5419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ ((1^st ‘𝑦) = (1^st ‘𝑥) ∧ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
370	369	baib 535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1^st ‘𝑦) = (1^st ‘𝑥) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
371	359, 370	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
372	367, 371	bitrd 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2^nd ‘𝑦) = (2^nd ‘𝑥)))
373	372	necon3bid 2973	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
374	365, 373	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ≠ (2^nd ‘𝑥))
375		eldifsn 4737	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ↔ ((2^nd ‘𝑦) ∈ (𝐴 “ {(1^st ‘𝑥)}) ∧ (2^nd ‘𝑦) ≠ (2^nd ‘𝑥)))
376	364, 374, 375	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2^nd ‘𝑦) ∈ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
377		ovex 7385	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ V
378		difss 4085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}) ⊆ (𝐴 “ {(1^st ‘𝑥)})
379		resmpt 5990	. . . . . . . . . . . . . . . . . . 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 7360	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (2^nd ‘𝑦) → ((1^st ‘𝑥)𝑆𝑗) = ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)))
382	380, 381	elrnmpt1s 5903	. . . . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1^st ‘𝑥)𝑆(2^nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
384	361, 383	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
385		df-ima 5632	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))
386	384, 385	eleqtrrdi 2844	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
387	386	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1^st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
388	346, 387	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
389	388	ralrimiv 3124	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
390	231, 250	sstrid 3942	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391		funimass4 6892	. . . . . . . . . . . 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 584	. . . . . . . . . . 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 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
394	393	unissd 4868	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))
395		imassrn 6024	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))
396	395, 267	sstrid 3942	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397		sspwuni 5050	. . . . . . . . . 10 ⊢ (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
398	396, 397	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})) ⊆ (Base‘𝐺))
399	166, 3, 394, 398	mrcssd 17532	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)}))))
400		ss2in 4194	. . . . . . . 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 584	. . . . . . 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 19925	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗))‘(2^nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1^st ‘𝑥)}) ↦ ((1^st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1^st ‘𝑥)}) ∖ {(2^nd ‘𝑥)})))) = {(0_g‘𝐺)})
404	401, 403	sseqtrd 3967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
405	2	subg0cl 19049	. . . . . . . . 9 ⊢ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
406	222, 405	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))))
407	333, 406	elind 4149	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0_g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
408	407	snssd 4760	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0_g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))))
409	404, 408	eqssd 3948	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))) = {(0_g‘𝐺)})
410	340, 409	eqtrid 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0_g‘𝐺)})
411	225, 222, 310, 224, 2, 339, 410	lsmdisj2 19596	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1^st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1^st ‘𝑥)})))))) = {(0_g‘𝐺)})
412	309, 411	sseqtrd 3967	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
413	1, 2, 3, 6, 40, 41, 162, 412	dmdprdd 19915	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 Vcvv 3437 ∖ cdif 3895 ∪ cun 3896 ∩ cin 3897 ⊆ wss 3898 ∅c0 4282 𝒫 cpw 4549 {csn 4575 ⟨cop 4581 ∪ cuni 4858 ∪ ciun 4941 class class class wbr 5093 ↦ cmpt 5174 × cxp 5617 dom cdm 5619 ran crn 5620 ↾ cres 5621 “ cima 5622 Rel wrel 5624 Fun wfun 6480 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 (class class class)co 7352 1^st c1st 7925 2^nd c2nd 7926 Basecbs 17122 0_gc0g 17345 Moorecmre 17486 mrClscmrc 17487 ACScacs 17489 Grpcgrp 18848 SubGrpcsubg 19035 Cntzccntz 19229 LSSumclsm 19548 DProd cdprd 19909

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-supp 8097 df-tpos 8162 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-2o 8392 df-er 8628 df-map 8758 df-ixp 8828 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-fsupp 9253 df-oi 9403 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-nn 12133 df-2 12195 df-n0 12389 df-z 12476 df-uz 12739 df-fz 13410 df-fzo 13557 df-seq 13911 df-hash 14240 df-sets 17077 df-slot 17095 df-ndx 17107 df-base 17123 df-ress 17144 df-plusg 17176 df-0g 17347 df-gsum 17348 df-mre 17490 df-mrc 17491 df-acs 17493 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-mhm 18693 df-submnd 18694 df-grp 18851 df-minusg 18852 df-sbg 18853 df-mulg 18983 df-subg 19038 df-ghm 19127 df-gim 19173 df-cntz 19231 df-oppg 19260 df-lsm 19550 df-cmn 19696 df-dprd 19911

This theorem is referenced by: dprd2db 19959 dprd2d2 19960

W3C validator