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

Theorem dprd2da 20042
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 2726 . 2 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2726 . 2 (0g𝐺) = (0g𝐺)
3 dprd2d.k . 2 𝐾 = (mrCls‘(SubGrp‘𝐺))
4 dprd2d.5 . . 3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5 dprdgrp 20005 . . 3 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
64, 5syl 17 . 2 (𝜑𝐺 ∈ Grp)
7 resiun2 6010 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = 𝑖𝐼 (𝐴 ↾ {𝑖})
8 iunid 5068 . . . . . 6 𝑖𝐼 {𝑖} = 𝐼
98reseq2i 5986 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = (𝐴𝐼)
107, 9eqtr3i 2756 . . . 4 𝑖𝐼 (𝐴 ↾ {𝑖}) = (𝐴𝐼)
11 dprd2d.1 . . . . 5 (𝜑 → Rel 𝐴)
12 dprd2d.3 . . . . 5 (𝜑 → dom 𝐴𝐼)
13 relssres 6031 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝐼) → (𝐴𝐼) = 𝐴)
1411, 12, 13syl2anc 582 . . . 4 (𝜑 → (𝐴𝐼) = 𝐴)
1510, 14eqtrid 2778 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16 ovex 7457 . . . . . 6 (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17 eqid 2726 . . . . . 6 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
1816, 17dmmpti 6705 . . . . 5 dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19 reldmdprd 19997 . . . . . . 7 Rel dom DProd
2019brrelex2i 5739 . . . . . 6 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21 dmexg 7914 . . . . . 6 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
224, 20, 213syl 18 . . . . 5 (𝜑 → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
2318, 22eqeltrrid 2831 . . . 4 (𝜑𝐼 ∈ V)
24 ressn 6296 . . . . . 6 (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25 vsnex 5435 . . . . . . 7 {𝑖} ∈ V
26 ovex 7457 . . . . . . . . 9 (𝑖𝑆𝑗) ∈ V
27 eqid 2726 . . . . . . . . 9 (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
2826, 27dmmpti 6705 . . . . . . . 8 dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29 dprd2d.4 . . . . . . . . 9 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
3019brrelex2i 5739 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31 dmexg 7914 . . . . . . . . 9 ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3229, 30, 313syl 18 . . . . . . . 8 ((𝜑𝑖𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3328, 32eqeltrrid 2831 . . . . . . 7 ((𝜑𝑖𝐼) → (𝐴 “ {𝑖}) ∈ V)
34 xpexg 7758 . . . . . . 7 (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3525, 33, 34sylancr 585 . . . . . 6 ((𝜑𝑖𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3624, 35eqeltrid 2830 . . . . 5 ((𝜑𝑖𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
3736ralrimiva 3136 . . . 4 (𝜑 → ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38 iunexg 7977 . . . 4 ((𝐼 ∈ V ∧ ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V) → 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
3923, 37, 38syl2anc 582 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
4015, 39eqeltrrd 2827 . 2 (𝜑𝐴 ∈ V)
41 dprd2d.2 . 2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
42 sneq 4643 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → {𝑖} = {(1st𝑥)})
4342imaeq2d 6069 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑥)}))
44 oveq1 7431 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝑖𝑆𝑗) = ((1st𝑥)𝑆𝑗))
4543, 44mpteq12dv 5244 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
4645breq2d 5165 . . . . . . . 8 (𝑖 = (1st𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
4729ralrimiva 3136 . . . . . . . . 9 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4847adantr 479 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4912adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐴) → dom 𝐴𝐼)
50 1stdm 8054 . . . . . . . . . 10 ((Rel 𝐴𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5111, 50sylan 578 . . . . . . . . 9 ((𝜑𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5249, 51sseldd 3980 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥) ∈ 𝐼)
5346, 48, 52rspcdva 3609 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
54533ad2antr1 1185 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5554adantr 479 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
56 ovex 7457 . . . . . . 7 ((1st𝑥)𝑆𝑗) ∈ V
57 eqid 2726 . . . . . . 7 (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
5856, 57dmmpti 6705 . . . . . 6 dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)})
5958a1i 11 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
60 1st2nd 8053 . . . . . . . . . . 11 ((Rel 𝐴𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6111, 60sylan 578 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
62 simpr 483 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴)
6361, 62eqeltrrd 2827 . . . . . . . . 9 ((𝜑𝑥𝐴) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
64 df-br 5154 . . . . . . . . 9 ((1st𝑥)𝐴(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
6563, 64sylibr 233 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥)𝐴(2nd𝑥))
6611adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐴) → Rel 𝐴)
67 elrelimasn 6095 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6866, 67syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6965, 68mpbird 256 . . . . . . 7 ((𝜑𝑥𝐴) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
70693ad2antr1 1185 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7170adantr 479 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7211adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → Rel 𝐴)
73 simpr2 1192 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦𝐴)
74 1st2nd 8053 . . . . . . . . . . 11 ((Rel 𝐴𝑦𝐴) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7572, 73, 74syl2anc 582 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7675, 73eqeltrrd 2827 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
77 df-br 5154 . . . . . . . . 9 ((1st𝑦)𝐴(2nd𝑦) ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
7876, 77sylibr 233 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦)𝐴(2nd𝑦))
79 elrelimasn 6095 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8072, 79syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8178, 80mpbird 256 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
8281adantr 479 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
83 simpr 483 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (1st𝑥) = (1st𝑦))
8483sneqd 4645 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → {(1st𝑥)} = {(1st𝑦)})
8584imaeq2d 6069 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝐴 “ {(1st𝑥)}) = (𝐴 “ {(1st𝑦)}))
8682, 85eleqtrrd 2829 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
87 simplr3 1214 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝑥𝑦)
88 simpr1 1191 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥𝐴)
8972, 88, 60syl2anc 582 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
9089, 75eqeq12d 2742 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩))
91 fvex 6914 . . . . . . . . . 10 (1st𝑥) ∈ V
92 fvex 6914 . . . . . . . . . 10 (2nd𝑥) ∈ V
9391, 92opth 5482 . . . . . . . . 9 (⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦)))
9490, 93bitrdi 286 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦))))
9594baibd 538 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥 = 𝑦 ↔ (2nd𝑥) = (2nd𝑦)))
9695necon3bid 2975 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥𝑦 ↔ (2nd𝑥) ≠ (2nd𝑦)))
9787, 96mpbid 231 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ≠ (2nd𝑦))
9855, 59, 71, 86, 97, 1dprdcntz 20008 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))))
99 df-ov 7427 . . . . . 6 ((1st𝑥)𝑆(2nd𝑥)) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩)
100 oveq2 7432 . . . . . . . 8 (𝑗 = (2nd𝑥) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑥)))
101100, 57, 56fvmpt3i 7014 . . . . . . 7 ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10270, 101syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10389fveq2d 6905 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
10499, 102, 1033eqtr4a 2792 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
105104adantr 479 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
10683oveq1d 7439 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((1st𝑥)𝑆𝑗) = ((1st𝑦)𝑆𝑗))
10785, 106mpteq12dv 5244 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
108107fveq1d 6903 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)))
109 df-ov 7427 . . . . . . . 8 ((1st𝑦)𝑆(2nd𝑦)) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩)
110 oveq2 7432 . . . . . . . . . 10 (𝑗 = (2nd𝑦) → ((1st𝑦)𝑆𝑗) = ((1st𝑦)𝑆(2nd𝑦)))
111 eqid 2726 . . . . . . . . . 10 (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))
112 ovex 7457 . . . . . . . . . 10 ((1st𝑦)𝑆𝑗) ∈ V
113110, 111, 112fvmpt3i 7014 . . . . . . . . 9 ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11481, 113syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11575fveq2d 6905 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
116109, 114, 1153eqtr4a 2792 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
117116adantr 479 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
118108, 117eqtrd 2766 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
119118fveq2d 6905 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))) = ((Cntz‘𝐺)‘(𝑆𝑦)))
12098, 105, 1193sstr3d 4026 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
12111, 41, 12, 29, 4, 3dprd2dlem2 20040 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12245oveq2d 7440 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
123122, 17, 16fvmpt3i 7014 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12452, 123syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
125121, 124sseqtrrd 4021 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1261253ad2antr1 1185 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
127126adantr 479 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1284ad2antrr 724 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
12918a1i 11 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
130523ad2antr1 1185 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑥) ∈ 𝐼)
131130adantr 479 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ∈ 𝐼)
13212adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom 𝐴𝐼)
133 1stdm 8054 . . . . . . . . 9 ((Rel 𝐴𝑦𝐴) → (1st𝑦) ∈ dom 𝐴)
13472, 73, 133syl2anc 582 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ dom 𝐴)
135132, 134sseldd 3980 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ 𝐼)
136135adantr 479 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑦) ∈ 𝐼)
137 simpr 483 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ≠ (1st𝑦))
138128, 129, 131, 136, 137, 1dprdcntz 20008 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))))
139 sneq 4643 . . . . . . . . . . . . 13 (𝑖 = (1st𝑦) → {𝑖} = {(1st𝑦)})
140139imaeq2d 6069 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑦)}))
141 oveq1 7431 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝑖𝑆𝑗) = ((1st𝑦)𝑆𝑗))
142140, 141mpteq12dv 5244 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
143142oveq2d 7440 . . . . . . . . . 10 (𝑖 = (1st𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
144143, 17, 16fvmpt3i 7014 . . . . . . . . 9 ((1st𝑦) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
145135, 144syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
146145fveq2d 6905 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))))
147 eqid 2726 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
148147dprdssv 20016 . . . . . . . 8 (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149142breq2d 5165 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
15047adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151149, 150, 135rspcdva 3609 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
152112, 111dmmpti 6705 . . . . . . . . . . 11 dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)})
153152a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)}))
154151, 153, 81dprdub 20025 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
155116, 154eqsstrrd 4019 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
156147, 1cntz2ss 19329 . . . . . . . 8 (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
157148, 155, 156sylancr 585 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
158146, 157eqsstrd 4018 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
159158adantr 479 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
160138, 159sstrd 3990 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
161127, 160sstrd 3990 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
162120, 161pm2.61dane 3019 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
1636adantr 479 . . . . . 6 ((𝜑𝑥𝐴) → 𝐺 ∈ Grp)
164147subgacs 19155 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165 acsmre 17665 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166163, 164, 1653syl 18 . . . . 5 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
16714adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = 𝐴)
168 undif2 4481 . . . . . . . . . . . . . . . . . 18 ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})) = ({(1st𝑥)} ∪ 𝐼)
16952snssd 4818 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → {(1st𝑥)} ⊆ 𝐼)
170 ssequn1 4181 . . . . . . . . . . . . . . . . . . 19 ({(1st𝑥)} ⊆ 𝐼 ↔ ({(1st𝑥)} ∪ 𝐼) = 𝐼)
171169, 170sylib 217 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∪ 𝐼) = 𝐼)
172168, 171eqtr2id 2779 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐼 = ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})))
173172reseq2d 5989 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
174167, 173eqtr3d 2768 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐴 = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
175 resundi 6003 . . . . . . . . . . . . . . 15 (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))) = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
176174, 175eqtrdi 2782 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
177176difeq1d 4120 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}))
178 difundir 4282 . . . . . . . . . . . . 13 (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
179177, 178eqtrdi 2782 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})))
180 neirr 2939 . . . . . . . . . . . . . . . . 17 ¬ (1st𝑥) ≠ (1st𝑥)
18161eleq1d 2811 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
182 df-br 5154 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
18392brresi 5998 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) ∧ (1st𝑥)𝐴(2nd𝑥)))
184183simplbi 496 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}))
185 eldifsni 4799 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) → (1st𝑥) ≠ (1st𝑥))
186184, 185syl 17 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ≠ (1st𝑥))
187182, 186sylbir 234 . . . . . . . . . . . . . . . . . 18 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥))
188181, 187biimtrdi 252 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥)))
189180, 188mtoi 198 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
190 disjsn 4720 . . . . . . . . . . . . . . . 16 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
191189, 190sylibr 233 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅)
192 disj3 4458 . . . . . . . . . . . . . . 15 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
193191, 192sylib 217 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
194193eqcomd 2732 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
195194uneq2d 4163 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
196179, 195eqtrd 2766 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
197196imaeq2d 6069 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
198 imaundi 6161 . . . . . . . . . 10 (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
199197, 198eqtrdi 2782 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
200199unieqd 4926 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
201 uniun 4938 . . . . . . . 8 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
202200, 201eqtrdi 2782 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
203 imassrn 6080 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
20441frnd 6736 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205204adantr 479 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206 mresspw 17605 . . . . . . . . . . . . 13 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207166, 206syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208205, 207sstrd 3990 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209203, 208sstrid 3991 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210 sspwuni 5108 . . . . . . . . . 10 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211209, 210sylib 217 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212166, 3, 211mrcssidd 17638 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
213 imassrn 6080 . . . . . . . . . . 11 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ ran 𝑆
214213, 208sstrid 3991 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215 sspwuni 5108 . . . . . . . . . 10 ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
216214, 215sylib 217 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
217166, 3, 216mrcssidd 17638 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
218 unss12 4183 . . . . . . . 8 (( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
219212, 217, 218syl2anc 582 . . . . . . 7 ((𝜑𝑥𝐴) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
220202, 219eqsstrd 4018 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
2213mrccl 17624 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222166, 211, 221syl2anc 582 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
2233mrccl 17624 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
224166, 216, 223syl2anc 582 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
225 eqid 2726 . . . . . . . 8 (LSSum‘𝐺) = (LSSum‘𝐺)
226225lsmunss 19657 . . . . . . 7 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
227222, 224, 226syl2anc 582 . . . . . 6 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
228220, 227sstrd 3990 . . . . 5 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
229 difss 4131 . . . . . . . . . . . . 13 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st𝑥)})
230 ressn 6296 . . . . . . . . . . . . 13 (𝐴 ↾ {(1st𝑥)}) = ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
231229, 230sseqtri 4016 . . . . . . . . . . . 12 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
232 imass2 6112 . . . . . . . . . . . 12 (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))))
233231, 232ax-mp 5 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
234 ovex 7457 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝑆𝑖) ∈ V
235 oveq2 7432 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆𝑖))
23657, 235elrnmpt1s 5963 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝐴 “ {(1st𝑥)}) ∧ ((1st𝑥)𝑆𝑖) ∈ V) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
237234, 236mpan2 689 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝐴 “ {(1st𝑥)}) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
238237rgen 3053 . . . . . . . . . . . . . 14 𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
239238a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
240 oveq1 7431 . . . . . . . . . . . . . . . 16 (𝑦 = (1st𝑥) → (𝑦𝑆𝑖) = ((1st𝑥)𝑆𝑖))
241240eleq1d 2811 . . . . . . . . . . . . . . 15 (𝑦 = (1st𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
242241ralbidv 3168 . . . . . . . . . . . . . 14 (𝑦 = (1st𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
24391, 242ralsn 4690 . . . . . . . . . . . . 13 (∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
244239, 243sylibr 233 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
24541adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
246245ffund 6732 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun 𝑆)
247 resss 6011 . . . . . . . . . . . . . . 15 (𝐴 ↾ {(1st𝑥)}) ⊆ 𝐴
248230, 247eqsstrri 4015 . . . . . . . . . . . . . 14 ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ 𝐴
249245fdmd 6738 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → dom 𝑆 = 𝐴)
250248, 249sseqtrrid 4033 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆)
251 funimassov 7603 . . . . . . . . . . . . 13 ((Fun 𝑆 ∧ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
252246, 250, 251syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
253244, 252mpbird 256 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
254233, 253sstrid 3991 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
255254unissd 4923 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
256 df-ov 7427 . . . . . . . . . . . . . 14 ((1st𝑥)𝑆𝑗) = (𝑆‘⟨(1st𝑥), 𝑗⟩)
25741ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258 elrelimasn 6095 . . . . . . . . . . . . . . . . . 18 (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
25966, 258syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
260259biimpa 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (1st𝑥)𝐴𝑗)
261 df-br 5154 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝐴𝑗 ↔ ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
262260, 261sylib 217 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
263257, 262ffvelcdmd 7099 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (𝑆‘⟨(1st𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
264256, 263eqeltrid 2830 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ((1st𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265264fmpttd 7129 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺))
266265frnd 6736 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267266, 207sstrd 3990 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268 sspwuni 5108 . . . . . . . . . 10 (ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
269267, 268sylib 217 . . . . . . . . 9 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
270166, 3, 255, 269mrcssd 17637 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2713dprdspan 20027 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27253, 271syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
273270, 272sseqtrrd 4021 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27416, 17fnmpti 6704 . . . . . . . . . . . . 13 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275 fnressn 7172 . . . . . . . . . . . . 13 (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st𝑥) ∈ 𝐼) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
276274, 52, 275sylancr 585 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
277124opeq2d 4886 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩ = ⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩)
278277sneqd 4645 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩} = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
279276, 278eqtrd 2766 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
280279oveq2d 7440 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}))
281 dprdsubg 20024 . . . . . . . . . . . . 13 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
28253, 281syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
283 dprdsn 20036 . . . . . . . . . . . 12 (((1st𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
28452, 282, 283syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
285284simprd 494 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
286280, 285eqtrd 2766 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2874adantr 479 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
28818a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
289 difss 4131 . . . . . . . . . . 11 (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼
290289a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼)
291 disjdif 4476 . . . . . . . . . . 11 ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅
292291a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅)
293287, 288, 169, 290, 292, 1dprdcntz2 20038 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
294286, 293eqsstrrd 4019 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
29529adantlr 713 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
29666, 245, 49, 295, 287, 3, 290dprd2dlem1 20041 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297 resmpt 6046 . . . . . . . . . . . 12 ((𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
298289, 297ax-mp 5 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
299298oveq2i 7435 . . . . . . . . . 10 (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300296, 299eqtr4di 2784 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
301300fveq2d 6905 . . . . . . . 8 ((𝜑𝑥𝐴) → ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
302294, 301sseqtrrd 4021 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
303273, 302sstrd 3990 . . . . . 6 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
304225, 1lsmsubg 19652 . . . . . 6 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
305222, 224, 303, 304syl3anc 1368 . . . . 5 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
3063mrcsscl 17633 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∧ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
307166, 228, 305, 306syl3anc 1368 . . . 4 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
308 sslin 4236 . . . 4 ((𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
309307, 308syl 17 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
31041ffvelcdmda 7098 . . . 4 ((𝜑𝑥𝐴) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
311225lsmlub 19662 . . . . . . . . . 10 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
312222, 310, 282, 311syl3anc 1368 . . . . . . . . 9 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
313273, 121, 312mpbi2and 710 . . . . . . . 8 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
314313, 124sseqtrrd 4021 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
315287, 288, 290dprdres 20028 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) ∧ (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
316315simpld 493 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
3173dprdspan 20027 . . . . . . . . . . 11 (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
318316, 317syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
319 df-ima 5695 . . . . . . . . . . . 12 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
320319unieqi 4925 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
321320fveq2i 6904 . . . . . . . . . 10 (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
322318, 321eqtr4di 2784 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
323300, 322eqtrd 2766 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
324 eqimss 4038 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
325323, 324syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
326 ss2in 4238 . . . . . . 7 ((((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
327314, 325, 326syl2anc 582 . . . . . 6 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
328287, 288, 52, 2, 3dprddisj 20009 . . . . . 6 ((𝜑𝑥𝐴) → (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) = {(0g𝐺)})
329327, 328sseqtrd 4020 . . . . 5 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ {(0g𝐺)})
330225lsmub2 19656 . . . . . . . . 9 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺)) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
331222, 310, 330syl2anc 582 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3322subg0cl 19128 . . . . . . . . 9 ((𝑆𝑥) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑆𝑥))
333310, 332syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝑆𝑥))
334331, 333sseldd 3980 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3352subg0cl 19128 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
336224, 335syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
337334, 336elind 4195 . . . . . 6 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
338337snssd 4818 . . . . 5 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
339329, 338eqssd 3997 . . . 4 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = {(0g𝐺)})
340 incom 4202 . . . . 5 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
34169, 101syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
34261fveq2d 6905 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
34399, 341, 3423eqtr4a 2792 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
344 eqimss2 4039 . . . . . . . . 9 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
345343, 344syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
346 eldifsn 4795 . . . . . . . . . . . . 13 (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥))
34711ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → Rel 𝐴)
348 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st𝑥)}))
349247, 348sselid 3977 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝐴)
350347, 349, 74syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
351350fveq2d 6905 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
352351, 109eqtr4di 2784 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑦)𝑆(2nd𝑦)))
353350, 348eqeltrrd 2827 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}))
354 fvex 6914 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑦) ∈ V
355354opelresi 5997 . . . . . . . . . . . . . . . . . . . . 21 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) ↔ ((1st𝑦) ∈ {(1st𝑥)} ∧ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴))
356355simplbi 496 . . . . . . . . . . . . . . . . . . . 20 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) → (1st𝑦) ∈ {(1st𝑥)})
357353, 356syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) ∈ {(1st𝑥)})
358 elsni 4650 . . . . . . . . . . . . . . . . . . 19 ((1st𝑦) ∈ {(1st𝑥)} → (1st𝑦) = (1st𝑥))
359357, 358syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) = (1st𝑥))
360359oveq1d 7439 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑦)𝑆(2nd𝑦)) = ((1st𝑥)𝑆(2nd𝑦)))
361352, 360eqtrd 2766 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑥)𝑆(2nd𝑦)))
362348, 230eleqtrdi 2836 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
363 xp2nd 8036 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
364362, 363syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
365 simprr 771 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝑥)
36661adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
367350, 366eqeq12d 2742 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩))
368 fvex 6914 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑦) ∈ V
369368, 354opth 5482 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ ((1st𝑦) = (1st𝑥) ∧ (2nd𝑦) = (2nd𝑥)))
370369baib 534 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑦) = (1st𝑥) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
371359, 370syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
372367, 371bitrd 278 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ (2nd𝑦) = (2nd𝑥)))
373372necon3bid 2975 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦𝑥 ↔ (2nd𝑦) ≠ (2nd𝑥)))
374365, 373mpbid 231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ≠ (2nd𝑥))
375 eldifsn 4795 . . . . . . . . . . . . . . . . . 18 ((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↔ ((2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}) ∧ (2nd𝑦) ≠ (2nd𝑥)))
376364, 374, 375sylanbrc 581 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
377 ovex 7457 . . . . . . . . . . . . . . . . 17 ((1st𝑥)𝑆(2nd𝑦)) ∈ V
378 difss 4131 . . . . . . . . . . . . . . . . . . 19 ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)})
379 resmpt 6046 . . . . . . . . . . . . . . . . . . 19 (((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
380378, 379ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
381 oveq2 7432 . . . . . . . . . . . . . . . . . 18 (𝑗 = (2nd𝑦) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑦)))
382380, 381elrnmpt1s 5963 . . . . . . . . . . . . . . . . 17 (((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ∧ ((1st𝑥)𝑆(2nd𝑦)) ∈ V) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
383376, 377, 382sylancl 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
384361, 383eqeltrd 2826 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
385 df-ima 5695 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
386384, 385eleqtrrdi 2837 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
387386ex 411 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
388346, 387biimtrid 241 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
389388ralrimiv 3135 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
390231, 250sstrid 3991 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391 funimass4 6967 . . . . . . . . . . . 12 ((Fun 𝑆 ∧ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
392246, 390, 391syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
393389, 392mpbird 256 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
394393unissd 4923 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
395 imassrn 6080 . . . . . . . . . . 11 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
396395, 267sstrid 3991 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397 sspwuni 5108 . . . . . . . . . 10 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
398396, 397sylib 217 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
399166, 3, 394, 398mrcssd 17637 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
400 ss2in 4238 . . . . . . . 8 (((𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
401345, 399, 400syl2anc 582 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
40258a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
40353, 402, 69, 2, 3dprddisj 20009 . . . . . . 7 ((𝜑𝑥𝐴) → (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) = {(0g𝐺)})
404401, 403sseqtrd 4020 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ {(0g𝐺)})
4052subg0cl 19128 . . . . . . . . 9 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
406222, 405syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
407333, 406elind 4195 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
408407snssd 4818 . . . . . 6 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
409404, 408eqssd 3997 . . . . 5 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) = {(0g𝐺)})
410340, 409eqtrid 2778 . . . 4 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = {(0g𝐺)})
411225, 222, 310, 224, 2, 339, 410lsmdisj2 19680 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) = {(0g𝐺)})
412309, 411sseqtrd 4020 . 2 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g𝐺)})
4131, 2, 3, 6, 40, 41, 162, 412dmdprdd 19999 1 (𝜑𝐺dom DProd 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  Vcvv 3462  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  𝒫 cpw 4607  {csn 4633  cop 4639   cuni 4913   ciun 5001   class class class wbr 5153  cmpt 5236   × cxp 5680  dom cdm 5682  ran crn 5683  cres 5684  cima 5685  Rel wrel 5687  Fun wfun 6548   Fn wfn 6549  wf 6550  cfv 6554  (class class class)co 7424  1st c1st 8001  2nd c2nd 8002  Basecbs 17213  0gc0g 17454  Moorecmre 17595  mrClscmrc 17596  ACScacs 17598  Grpcgrp 18928  SubGrpcsubg 19114  Cntzccntz 19309  LSSumclsm 19632   DProd cdprd 19993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-supp 8175  df-tpos 8241  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9406  df-oi 9553  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-nn 12265  df-2 12327  df-n0 12525  df-z 12611  df-uz 12875  df-fz 13539  df-fzo 13682  df-seq 14022  df-hash 14348  df-sets 17166  df-slot 17184  df-ndx 17196  df-base 17214  df-ress 17243  df-plusg 17279  df-0g 17456  df-gsum 17457  df-mre 17599  df-mrc 17600  df-acs 17602  df-mgm 18633  df-sgrp 18712  df-mnd 18728  df-mhm 18773  df-submnd 18774  df-grp 18931  df-minusg 18932  df-sbg 18933  df-mulg 19062  df-subg 19117  df-ghm 19207  df-gim 19253  df-cntz 19311  df-oppg 19340  df-lsm 19634  df-cmn 19780  df-dprd 19995
This theorem is referenced by:  dprd2db  20043  dprd2d2  20044
  Copyright terms: Public domain W3C validator