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

Theorem dprd2da 18655
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.
StepHypRef Expression
1 eqid 2769 . 2 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2769 . 2 (0g𝐺) = (0g𝐺)
3 dprd2d.k . 2 𝐾 = (mrCls‘(SubGrp‘𝐺))
4 dprd2d.5 . . 3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5 dprdgrp 18618 . . 3 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
64, 5syl 17 . 2 (𝜑𝐺 ∈ Grp)
7 resiun2 5558 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = 𝑖𝐼 (𝐴 ↾ {𝑖})
8 iunid 4706 . . . . . 6 𝑖𝐼 {𝑖} = 𝐼
98reseq2i 5530 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = (𝐴𝐼)
107, 9eqtr3i 2793 . . . 4 𝑖𝐼 (𝐴 ↾ {𝑖}) = (𝐴𝐼)
11 dprd2d.1 . . . . 5 (𝜑 → Rel 𝐴)
12 dprd2d.3 . . . . 5 (𝜑 → dom 𝐴𝐼)
13 relssres 5577 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝐼) → (𝐴𝐼) = 𝐴)
1411, 12, 13syl2anc 693 . . . 4 (𝜑 → (𝐴𝐼) = 𝐴)
1510, 14syl5eq 2815 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16 ovex 6821 . . . . . 6 (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17 eqid 2769 . . . . . 6 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
1816, 17dmmpti 6162 . . . . 5 dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19 reldmdprd 18610 . . . . . . 7 Rel dom DProd
2019brrelex2i 5298 . . . . . 6 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21 dmexg 7242 . . . . . 6 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
224, 20, 213syl 18 . . . . 5 (𝜑 → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
2318, 22syl5eqelr 2853 . . . 4 (𝜑𝐼 ∈ V)
24 ressn 5814 . . . . . 6 (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25 snex 5035 . . . . . . 7 {𝑖} ∈ V
26 ovex 6821 . . . . . . . . 9 (𝑖𝑆𝑗) ∈ V
27 eqid 2769 . . . . . . . . 9 (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
2826, 27dmmpti 6162 . . . . . . . 8 dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29 dprd2d.4 . . . . . . . . 9 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
3019brrelex2i 5298 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31 dmexg 7242 . . . . . . . . 9 ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3229, 30, 313syl 18 . . . . . . . 8 ((𝜑𝑖𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3328, 32syl5eqelr 2853 . . . . . . 7 ((𝜑𝑖𝐼) → (𝐴 “ {𝑖}) ∈ V)
34 xpexg 7105 . . . . . . 7 (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3525, 33, 34sylancr 695 . . . . . 6 ((𝜑𝑖𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3624, 35syl5eqel 2852 . . . . 5 ((𝜑𝑖𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
3736ralrimiva 3113 . . . 4 (𝜑 → ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38 iunexg 7288 . . . 4 ((𝐼 ∈ V ∧ ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V) → 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
3923, 37, 38syl2anc 693 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
4015, 39eqeltrrd 2849 . 2 (𝜑𝐴 ∈ V)
41 dprd2d.2 . 2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
42 sneq 4323 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → {𝑖} = {(1st𝑥)})
4342imaeq2d 5606 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑥)}))
44 oveq1 6798 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝑖𝑆𝑗) = ((1st𝑥)𝑆𝑗))
4543, 44mpteq12dv 4864 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
4645breq2d 4795 . . . . . . . 8 (𝑖 = (1st𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
4729ralrimiva 3113 . . . . . . . . 9 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4847adantr 473 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4912adantr 473 . . . . . . . . 9 ((𝜑𝑥𝐴) → dom 𝐴𝐼)
50 1stdm 7362 . . . . . . . . . 10 ((Rel 𝐴𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5111, 50sylan 490 . . . . . . . . 9 ((𝜑𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5249, 51sseldd 3750 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥) ∈ 𝐼)
5346, 48, 52rspcdva 3463 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
54533ad2antr1 1201 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5554adantr 473 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
56 ovex 6821 . . . . . . 7 ((1st𝑥)𝑆𝑗) ∈ V
57 eqid 2769 . . . . . . 7 (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
5856, 57dmmpti 6162 . . . . . 6 dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)})
5958a1i 11 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
60 1st2nd 7361 . . . . . . . . . . 11 ((Rel 𝐴𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6111, 60sylan 490 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
62 simpr 480 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴)
6361, 62eqeltrrd 2849 . . . . . . . . 9 ((𝜑𝑥𝐴) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
64 df-br 4784 . . . . . . . . 9 ((1st𝑥)𝐴(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
6563, 64sylibr 224 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥)𝐴(2nd𝑥))
6611adantr 473 . . . . . . . . 9 ((𝜑𝑥𝐴) → Rel 𝐴)
67 elrelimasn 5629 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6866, 67syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6965, 68mpbird 247 . . . . . . 7 ((𝜑𝑥𝐴) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
70693ad2antr1 1201 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7170adantr 473 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7211adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → Rel 𝐴)
73 simpr2 1233 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦𝐴)
74 1st2nd 7361 . . . . . . . . . . 11 ((Rel 𝐴𝑦𝐴) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7572, 73, 74syl2anc 693 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7675, 73eqeltrrd 2849 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
77 df-br 4784 . . . . . . . . 9 ((1st𝑦)𝐴(2nd𝑦) ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
7876, 77sylibr 224 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦)𝐴(2nd𝑦))
79 elrelimasn 5629 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8072, 79syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8178, 80mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
8281adantr 473 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
83 simpr 480 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (1st𝑥) = (1st𝑦))
8483sneqd 4325 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → {(1st𝑥)} = {(1st𝑦)})
8584imaeq2d 5606 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝐴 “ {(1st𝑥)}) = (𝐴 “ {(1st𝑦)}))
8682, 85eleqtrrd 2851 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
87 simplr3 1262 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝑥𝑦)
88 simpr1 1231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥𝐴)
8972, 88, 60syl2anc 693 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
9089, 75eqeq12d 2784 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩))
91 fvex 6341 . . . . . . . . . 10 (1st𝑥) ∈ V
92 fvex 6341 . . . . . . . . . 10 (2nd𝑥) ∈ V
9391, 92opth 5071 . . . . . . . . 9 (⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦)))
9490, 93syl6bb 276 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦))))
9594baibd 983 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥 = 𝑦 ↔ (2nd𝑥) = (2nd𝑦)))
9695necon3bid 2985 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥𝑦 ↔ (2nd𝑥) ≠ (2nd𝑦)))
9787, 96mpbid 222 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ≠ (2nd𝑦))
9855, 59, 71, 86, 97, 1dprdcntz 18621 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))))
99 df-ov 6794 . . . . . 6 ((1st𝑥)𝑆(2nd𝑥)) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩)
100 oveq2 6799 . . . . . . . 8 (𝑗 = (2nd𝑥) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑥)))
101100, 57, 56fvmpt3i 6428 . . . . . . 7 ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10270, 101syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10389fveq2d 6335 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
10499, 102, 1033eqtr4a 2829 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
105104adantr 473 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
10683oveq1d 6806 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((1st𝑥)𝑆𝑗) = ((1st𝑦)𝑆𝑗))
10785, 106mpteq12dv 4864 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
108107fveq1d 6333 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)))
109 df-ov 6794 . . . . . . . 8 ((1st𝑦)𝑆(2nd𝑦)) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩)
110 oveq2 6799 . . . . . . . . . 10 (𝑗 = (2nd𝑦) → ((1st𝑦)𝑆𝑗) = ((1st𝑦)𝑆(2nd𝑦)))
111 eqid 2769 . . . . . . . . . 10 (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))
112 ovex 6821 . . . . . . . . . 10 ((1st𝑦)𝑆𝑗) ∈ V
113110, 111, 112fvmpt3i 6428 . . . . . . . . 9 ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11481, 113syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11575fveq2d 6335 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
116109, 114, 1153eqtr4a 2829 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
117116adantr 473 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
118108, 117eqtrd 2803 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
119118fveq2d 6335 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))) = ((Cntz‘𝐺)‘(𝑆𝑦)))
12098, 105, 1193sstr3d 3793 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
12111, 41, 12, 29, 4, 3dprd2dlem2 18653 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12245oveq2d 6807 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
123122, 17, 16fvmpt3i 6428 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12452, 123syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
125121, 124sseqtr4d 3788 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1261253ad2antr1 1201 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
127126adantr 473 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1284ad2antrr 761 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
12918a1i 11 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
130523ad2antr1 1201 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑥) ∈ 𝐼)
131130adantr 473 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ∈ 𝐼)
13212adantr 473 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom 𝐴𝐼)
133 1stdm 7362 . . . . . . . . 9 ((Rel 𝐴𝑦𝐴) → (1st𝑦) ∈ dom 𝐴)
13472, 73, 133syl2anc 693 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ dom 𝐴)
135132, 134sseldd 3750 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ 𝐼)
136135adantr 473 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑦) ∈ 𝐼)
137 simpr 480 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ≠ (1st𝑦))
138128, 129, 131, 136, 137, 1dprdcntz 18621 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))))
139 sneq 4323 . . . . . . . . . . . . 13 (𝑖 = (1st𝑦) → {𝑖} = {(1st𝑦)})
140139imaeq2d 5606 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑦)}))
141 oveq1 6798 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝑖𝑆𝑗) = ((1st𝑦)𝑆𝑗))
142140, 141mpteq12dv 4864 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
143142oveq2d 6807 . . . . . . . . . 10 (𝑖 = (1st𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
144143, 17, 16fvmpt3i 6428 . . . . . . . . 9 ((1st𝑦) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
145135, 144syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
146145fveq2d 6335 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))))
147 eqid 2769 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
148147dprdssv 18629 . . . . . . . 8 (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149142breq2d 4795 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
15047adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151149, 150, 135rspcdva 3463 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
152112, 111dmmpti 6162 . . . . . . . . . . 11 dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)})
153152a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)}))
154151, 153, 81dprdub 18638 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
155116, 154eqsstr3d 3786 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
156147, 1cntz2ss 17978 . . . . . . . 8 (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
157148, 155, 156sylancr 695 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
158146, 157eqsstrd 3785 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
159158adantr 473 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
160138, 159sstrd 3759 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
161127, 160sstrd 3759 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
162120, 161pm2.61dane 3028 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
1636adantr 473 . . . . . 6 ((𝜑𝑥𝐴) → 𝐺 ∈ Grp)
164147subgacs 17843 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165 acsmre 16526 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166163, 164, 1653syl 18 . . . . 5 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
16714adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = 𝐴)
168 undif2 4183 . . . . . . . . . . . . . . . . . 18 ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})) = ({(1st𝑥)} ∪ 𝐼)
16952snssd 4472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → {(1st𝑥)} ⊆ 𝐼)
170 ssequn1 3931 . . . . . . . . . . . . . . . . . . 19 ({(1st𝑥)} ⊆ 𝐼 ↔ ({(1st𝑥)} ∪ 𝐼) = 𝐼)
171169, 170sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∪ 𝐼) = 𝐼)
172168, 171syl5req 2816 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐼 = ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})))
173172reseq2d 5533 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
174167, 173eqtr3d 2805 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐴 = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
175 resundi 5550 . . . . . . . . . . . . . . 15 (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))) = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
176174, 175syl6eq 2819 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
177176difeq1d 3875 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}))
178 difundir 4026 . . . . . . . . . . . . 13 (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
179177, 178syl6eq 2819 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})))
180 neirr 2950 . . . . . . . . . . . . . . . . 17 ¬ (1st𝑥) ≠ (1st𝑥)
18161eleq1d 2833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
182 df-br 4784 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
18392brres 5542 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ((1st𝑥)𝐴(2nd𝑥) ∧ (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)})))
184183simprbi 484 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}))
185 eldifsni 4454 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) → (1st𝑥) ≠ (1st𝑥))
186184, 185syl 17 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ≠ (1st𝑥))
187182, 186sylbir 225 . . . . . . . . . . . . . . . . . 18 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥))
188181, 187syl6bi 243 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥)))
189180, 188mtoi 190 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
190 disjsn 4380 . . . . . . . . . . . . . . . 16 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
191189, 190sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅)
192 disj3 4161 . . . . . . . . . . . . . . 15 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
193191, 192sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
194193eqcomd 2775 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
195194uneq2d 3915 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
196179, 195eqtrd 2803 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
197196imaeq2d 5606 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
198 imaundi 5685 . . . . . . . . . 10 (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
199197, 198syl6eq 2819 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
200199unieqd 4581 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
201 uniun 4590 . . . . . . . 8 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
202200, 201syl6eq 2819 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
203 imassrn 5617 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
204 frn 6192 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺))
20541, 204syl 17 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
206205adantr 473 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
207 mresspw 16466 . . . . . . . . . . . . 13 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208166, 207syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
209206, 208sstrd 3759 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
210203, 209syl5ss 3760 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
211 sspwuni 4742 . . . . . . . . . 10 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212210, 211sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
213166, 3, 212mrcssidd 16499 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
214 imassrn 5617 . . . . . . . . . . 11 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ ran 𝑆
215214, 209syl5ss 3760 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
216 sspwuni 4742 . . . . . . . . . 10 ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
217215, 216sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
218166, 3, 217mrcssidd 16499 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
219 unss12 3933 . . . . . . . 8 (( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
220213, 218, 219syl2anc 693 . . . . . . 7 ((𝜑𝑥𝐴) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
221202, 220eqsstrd 3785 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
2223mrccl 16485 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
223166, 212, 222syl2anc 693 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
2243mrccl 16485 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
225166, 217, 224syl2anc 693 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
226 eqid 2769 . . . . . . . 8 (LSSum‘𝐺) = (LSSum‘𝐺)
227226lsmunss 18286 . . . . . . 7 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
228223, 225, 227syl2anc 693 . . . . . 6 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
229221, 228sstrd 3759 . . . . 5 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
230 difss 3885 . . . . . . . . . . . . 13 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st𝑥)})
231 ressn 5814 . . . . . . . . . . . . 13 (𝐴 ↾ {(1st𝑥)}) = ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
232230, 231sseqtri 3783 . . . . . . . . . . . 12 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
233 imass2 5641 . . . . . . . . . . . 12 (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))))
234232, 233ax-mp 5 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
235 ovex 6821 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝑆𝑖) ∈ V
236 oveq2 6799 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆𝑖))
23757, 236elrnmpt1s 5510 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝐴 “ {(1st𝑥)}) ∧ ((1st𝑥)𝑆𝑖) ∈ V) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
238235, 237mpan2 706 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝐴 “ {(1st𝑥)}) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
239238rgen 3069 . . . . . . . . . . . . . 14 𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
240239a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
241 oveq1 6798 . . . . . . . . . . . . . . . 16 (𝑦 = (1st𝑥) → (𝑦𝑆𝑖) = ((1st𝑥)𝑆𝑖))
242241eleq1d 2833 . . . . . . . . . . . . . . 15 (𝑦 = (1st𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
243242ralbidv 3133 . . . . . . . . . . . . . 14 (𝑦 = (1st𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
24491, 243ralsn 4357 . . . . . . . . . . . . 13 (∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
245240, 244sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
24641adantr 473 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
247 ffun 6187 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆)
248246, 247syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun 𝑆)
249 resss 5562 . . . . . . . . . . . . . . 15 (𝐴 ↾ {(1st𝑥)}) ⊆ 𝐴
250231, 249eqsstr3i 3782 . . . . . . . . . . . . . 14 ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ 𝐴
251 fdm 6190 . . . . . . . . . . . . . . 15 (𝑆:𝐴⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐴)
252246, 251syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → dom 𝑆 = 𝐴)
253250, 252syl5sseqr 3800 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆)
254 funimassov 6956 . . . . . . . . . . . . 13 ((Fun 𝑆 ∧ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
255248, 253, 254syl2anc 693 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
256245, 255mpbird 247 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
257234, 256syl5ss 3760 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
258257unissd 4595 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
259 df-ov 6794 . . . . . . . . . . . . . 14 ((1st𝑥)𝑆𝑗) = (𝑆‘⟨(1st𝑥), 𝑗⟩)
26041ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
261 elrelimasn 5629 . . . . . . . . . . . . . . . . . 18 (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
26266, 261syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
263262biimpa 503 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (1st𝑥)𝐴𝑗)
264 df-br 4784 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝐴𝑗 ↔ ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
265263, 264sylib 208 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
266260, 265ffvelrnd 6502 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (𝑆‘⟨(1st𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
267259, 266syl5eqel 2852 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ((1st𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
268267, 57fmptd 6526 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺))
269 frn 6192 . . . . . . . . . . . 12 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
270268, 269syl 17 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
271270, 208sstrd 3759 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
272 sspwuni 4742 . . . . . . . . . 10 (ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
273271, 272sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
274166, 3, 258, 273mrcssd 16498 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2753dprdspan 18640 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27653, 275syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
277274, 276sseqtr4d 3788 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27816, 17fnmpti 6161 . . . . . . . . . . . . 13 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
279 fnressn 6566 . . . . . . . . . . . . 13 (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st𝑥) ∈ 𝐼) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
280278, 52, 279sylancr 695 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
281124opeq2d 4543 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩ = ⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩)
282281sneqd 4325 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩} = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
283280, 282eqtrd 2803 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
284283oveq2d 6807 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}))
285 dprdsubg 18637 . . . . . . . . . . . . 13 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
28653, 285syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
287 dprdsn 18649 . . . . . . . . . . . 12 (((1st𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
28852, 286, 287syl2anc 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
289288simprd 483 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
290284, 289eqtrd 2803 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2914adantr 473 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
29218a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
293 difss 3885 . . . . . . . . . . 11 (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼
294293a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼)
295 disjdif 4179 . . . . . . . . . . 11 ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅
296295a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅)
297291, 292, 169, 294, 296, 1dprdcntz2 18651 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
298290, 297eqsstr3d 3786 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
29929adantlr 750 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30066, 246, 49, 299, 291, 3, 294dprd2dlem1 18654 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
301 resmpt 5589 . . . . . . . . . . . 12 ((𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
302293, 301ax-mp 5 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
303302oveq2i 6802 . . . . . . . . . 10 (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
304300, 303syl6eqr 2821 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
305304fveq2d 6335 . . . . . . . 8 ((𝜑𝑥𝐴) → ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
306298, 305sseqtr4d 3788 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
307277, 306sstrd 3759 . . . . . 6 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
308226, 1lsmsubg 18282 . . . . . 6 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
309223, 225, 307, 308syl3anc 1474 . . . . 5 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
3103mrcsscl 16494 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∧ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
311166, 229, 309, 310syl3anc 1474 . . . 4 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
312 sslin 3984 . . . 4 ((𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
313311, 312syl 17 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
31441ffvelrnda 6501 . . . 4 ((𝜑𝑥𝐴) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
315226lsmlub 18291 . . . . . . . . . 10 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
316223, 314, 286, 315syl3anc 1474 . . . . . . . . 9 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
317277, 121, 316mpbi2and 991 . . . . . . . 8 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
318317, 124sseqtr4d 3788 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
319291, 292, 294dprdres 18641 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) ∧ (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
320319simpld 478 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
3213dprdspan 18640 . . . . . . . . . . 11 (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
322320, 321syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
323 df-ima 5261 . . . . . . . . . . . 12 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
324323unieqi 4580 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
325324fveq2i 6334 . . . . . . . . . 10 (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
326322, 325syl6eqr 2821 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
327304, 326eqtrd 2803 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
328 eqimss 3803 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
329327, 328syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
330 ss2in 3986 . . . . . . 7 ((((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
331318, 329, 330syl2anc 693 . . . . . 6 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
332291, 292, 52, 2, 3dprddisj 18622 . . . . . 6 ((𝜑𝑥𝐴) → (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) = {(0g𝐺)})
333331, 332sseqtrd 3787 . . . . 5 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ {(0g𝐺)})
334226lsmub2 18285 . . . . . . . . 9 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺)) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
335223, 314, 334syl2anc 693 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3362subg0cl 17816 . . . . . . . . 9 ((𝑆𝑥) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑆𝑥))
337314, 336syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝑆𝑥))
338335, 337sseldd 3750 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3392subg0cl 17816 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
340225, 339syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
341338, 340elind 3946 . . . . . 6 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
342341snssd 4472 . . . . 5 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
343333, 342eqssd 3766 . . . 4 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = {(0g𝐺)})
344 incom 3953 . . . . 5 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
34569, 101syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
34661fveq2d 6335 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
34799, 345, 3463eqtr4a 2829 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
348 eqimss2 3804 . . . . . . . . 9 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
349347, 348syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
350 eldifsn 4450 . . . . . . . . . . . . 13 (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥))
35111ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → Rel 𝐴)
352 simprl 808 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st𝑥)}))
353249, 352sseldi 3747 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝐴)
354351, 353, 74syl2anc 693 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
355354fveq2d 6335 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
356355, 109syl6eqr 2821 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑦)𝑆(2nd𝑦)))
357354, 352eqeltrrd 2849 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}))
358 fvex 6341 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑦) ∈ V
359358opelres 5541 . . . . . . . . . . . . . . . . . . . . 21 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) ↔ (⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴 ∧ (1st𝑦) ∈ {(1st𝑥)}))
360359simprbi 484 . . . . . . . . . . . . . . . . . . . 20 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) → (1st𝑦) ∈ {(1st𝑥)})
361357, 360syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) ∈ {(1st𝑥)})
362 elsni 4330 . . . . . . . . . . . . . . . . . . 19 ((1st𝑦) ∈ {(1st𝑥)} → (1st𝑦) = (1st𝑥))
363361, 362syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) = (1st𝑥))
364363oveq1d 6806 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑦)𝑆(2nd𝑦)) = ((1st𝑥)𝑆(2nd𝑦)))
365356, 364eqtrd 2803 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑥)𝑆(2nd𝑦)))
366352, 231syl6eleq 2858 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
367 xp2nd 7346 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
368366, 367syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
369 simprr 810 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝑥)
37061adantr 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
371354, 370eqeq12d 2784 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩))
372 fvex 6341 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑦) ∈ V
373372, 358opth 5071 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ ((1st𝑦) = (1st𝑥) ∧ (2nd𝑦) = (2nd𝑥)))
374373baib 979 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑦) = (1st𝑥) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
375363, 374syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
376371, 375bitrd 268 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ (2nd𝑦) = (2nd𝑥)))
377376necon3bid 2985 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦𝑥 ↔ (2nd𝑦) ≠ (2nd𝑥)))
378369, 377mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ≠ (2nd𝑥))
379 eldifsn 4450 . . . . . . . . . . . . . . . . . 18 ((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↔ ((2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}) ∧ (2nd𝑦) ≠ (2nd𝑥)))
380368, 378, 379sylanbrc 698 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
381 ovex 6821 . . . . . . . . . . . . . . . . 17 ((1st𝑥)𝑆(2nd𝑦)) ∈ V
382 difss 3885 . . . . . . . . . . . . . . . . . . 19 ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)})
383 resmpt 5589 . . . . . . . . . . . . . . . . . . 19 (((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
384382, 383ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
385 oveq2 6799 . . . . . . . . . . . . . . . . . 18 (𝑗 = (2nd𝑦) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑦)))
386384, 385elrnmpt1s 5510 . . . . . . . . . . . . . . . . 17 (((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ∧ ((1st𝑥)𝑆(2nd𝑦)) ∈ V) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
387380, 381, 386sylancl 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
388365, 387eqeltrd 2848 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
389 df-ima 5261 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
390388, 389syl6eleqr 2859 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
391390ex 448 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
392350, 391syl5bi 232 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
393392ralrimiv 3112 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
394232, 253syl5ss 3760 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
395 funimass4 6388 . . . . . . . . . . . 12 ((Fun 𝑆 ∧ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
396248, 394, 395syl2anc 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
397393, 396mpbird 247 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
398397unissd 4595 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
399 imassrn 5617 . . . . . . . . . . 11 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
400399, 271syl5ss 3760 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺))
401 sspwuni 4742 . . . . . . . . . 10 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
402400, 401sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
403166, 3, 398, 402mrcssd 16498 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
404 ss2in 3986 . . . . . . . 8 (((𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
405349, 403, 404syl2anc 693 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
40658a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
40753, 406, 69, 2, 3dprddisj 18622 . . . . . . 7 ((𝜑𝑥𝐴) → (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) = {(0g𝐺)})
408405, 407sseqtrd 3787 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ {(0g𝐺)})
4092subg0cl 17816 . . . . . . . . 9 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
410223, 409syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
411337, 410elind 3946 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
412411snssd 4472 . . . . . 6 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
413408, 412eqssd 3766 . . . . 5 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) = {(0g𝐺)})
414344, 413syl5eq 2815 . . . 4 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = {(0g𝐺)})
415226, 223, 314, 225, 2, 343, 414lsmdisj2 18308 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) = {(0g𝐺)})
416313, 415sseqtrd 3787 . 2 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g𝐺)})
4171, 2, 3, 6, 40, 41, 162, 416dmdprdd 18612 1 (𝜑𝐺dom DProd 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1069   = wceq 1629  wcel 2143  wne 2941  wral 3059  Vcvv 3348  cdif 3717  cun 3718  cin 3719  wss 3720  c0 4060  𝒫 cpw 4294  {csn 4313  cop 4319   cuni 4571   ciun 4651   class class class wbr 4783  cmpt 4860   × cxp 5246  dom cdm 5248  ran crn 5249  cres 5250  cima 5251  Rel wrel 5253  Fun wfun 6024   Fn wfn 6025  wf 6026  cfv 6030  (class class class)co 6791  1st c1st 7311  2nd c2nd 7312  Basecbs 16070  0gc0g 16314  Moorecmre 16456  mrClscmrc 16457  ACScacs 16459  Grpcgrp 17636  SubGrpcsubg 17802  Cntzccntz 17961  LSSumclsm 18262   DProd cdprd 18606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-rep 4901  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033  ax-un 7094  ax-inf2 8700  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1070  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ne 2942  df-nel 3045  df-ral 3064  df-rex 3065  df-reu 3066  df-rmo 3067  df-rab 3068  df-v 3350  df-sbc 3585  df-csb 3680  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-pss 3736  df-nul 4061  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4572  df-int 4609  df-iun 4653  df-iin 4654  df-br 4784  df-opab 4844  df-mpt 4861  df-tr 4884  df-id 5156  df-eprel 5161  df-po 5169  df-so 5170  df-fr 5207  df-se 5208  df-we 5209  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-rn 5259  df-res 5260  df-ima 5261  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-of 7042  df-om 7211  df-1st 7313  df-2nd 7314  df-supp 7445  df-tpos 7502  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-oadd 7715  df-er 7894  df-map 8009  df-ixp 8061  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-fsupp 8430  df-oi 8569  df-card 8963  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-nn 11221  df-2 11279  df-n0 11493  df-z 11578  df-uz 11888  df-fz 12533  df-fzo 12673  df-seq 13009  df-hash 13325  df-ndx 16073  df-slot 16074  df-base 16076  df-sets 16077  df-ress 16078  df-plusg 16168  df-0g 16316  df-gsum 16317  df-mre 16460  df-mrc 16461  df-acs 16463  df-mgm 17456  df-sgrp 17498  df-mnd 17509  df-mhm 17549  df-submnd 17550  df-grp 17639  df-minusg 17640  df-sbg 17641  df-mulg 17755  df-subg 17805  df-ghm 17872  df-gim 17915  df-cntz 17963  df-oppg 17989  df-lsm 18264  df-cmn 18408  df-dprd 18608
This theorem is referenced by:  dprd2db  18656  dprd2d2  18657
  Copyright terms: Public domain W3C validator