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

Theorem dprd2da 19161
 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 2798 . 2 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2798 . 2 (0g𝐺) = (0g𝐺)
3 dprd2d.k . 2 𝐾 = (mrCls‘(SubGrp‘𝐺))
4 dprd2d.5 . . 3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5 dprdgrp 19124 . . 3 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
64, 5syl 17 . 2 (𝜑𝐺 ∈ Grp)
7 resiun2 5840 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = 𝑖𝐼 (𝐴 ↾ {𝑖})
8 iunid 4948 . . . . . 6 𝑖𝐼 {𝑖} = 𝐼
98reseq2i 5816 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = (𝐴𝐼)
107, 9eqtr3i 2823 . . . 4 𝑖𝐼 (𝐴 ↾ {𝑖}) = (𝐴𝐼)
11 dprd2d.1 . . . . 5 (𝜑 → Rel 𝐴)
12 dprd2d.3 . . . . 5 (𝜑 → dom 𝐴𝐼)
13 relssres 5860 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝐼) → (𝐴𝐼) = 𝐴)
1411, 12, 13syl2anc 587 . . . 4 (𝜑 → (𝐴𝐼) = 𝐴)
1510, 14syl5eq 2845 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16 ovex 7169 . . . . . 6 (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17 eqid 2798 . . . . . 6 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
1816, 17dmmpti 6465 . . . . 5 dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19 reldmdprd 19116 . . . . . . 7 Rel dom DProd
2019brrelex2i 5574 . . . . . 6 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21 dmexg 7597 . . . . . 6 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
224, 20, 213syl 18 . . . . 5 (𝜑 → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
2318, 22eqeltrrid 2895 . . . 4 (𝜑𝐼 ∈ V)
24 ressn 6105 . . . . . 6 (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25 snex 5298 . . . . . . 7 {𝑖} ∈ V
26 ovex 7169 . . . . . . . . 9 (𝑖𝑆𝑗) ∈ V
27 eqid 2798 . . . . . . . . 9 (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
2826, 27dmmpti 6465 . . . . . . . 8 dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29 dprd2d.4 . . . . . . . . 9 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
3019brrelex2i 5574 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31 dmexg 7597 . . . . . . . . 9 ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3229, 30, 313syl 18 . . . . . . . 8 ((𝜑𝑖𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3328, 32eqeltrrid 2895 . . . . . . 7 ((𝜑𝑖𝐼) → (𝐴 “ {𝑖}) ∈ V)
34 xpexg 7456 . . . . . . 7 (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3525, 33, 34sylancr 590 . . . . . 6 ((𝜑𝑖𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3624, 35eqeltrid 2894 . . . . 5 ((𝜑𝑖𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
3736ralrimiva 3149 . . . 4 (𝜑 → ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38 iunexg 7649 . . . 4 ((𝐼 ∈ V ∧ ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V) → 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
3923, 37, 38syl2anc 587 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
4015, 39eqeltrrd 2891 . 2 (𝜑𝐴 ∈ V)
41 dprd2d.2 . 2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
42 sneq 4535 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → {𝑖} = {(1st𝑥)})
4342imaeq2d 5897 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑥)}))
44 oveq1 7143 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝑖𝑆𝑗) = ((1st𝑥)𝑆𝑗))
4543, 44mpteq12dv 5116 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
4645breq2d 5043 . . . . . . . 8 (𝑖 = (1st𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
4729ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4847adantr 484 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4912adantr 484 . . . . . . . . 9 ((𝜑𝑥𝐴) → dom 𝐴𝐼)
50 1stdm 7724 . . . . . . . . . 10 ((Rel 𝐴𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5111, 50sylan 583 . . . . . . . . 9 ((𝜑𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
5249, 51sseldd 3916 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥) ∈ 𝐼)
5346, 48, 52rspcdva 3573 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
54533ad2antr1 1185 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5554adantr 484 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
56 ovex 7169 . . . . . . 7 ((1st𝑥)𝑆𝑗) ∈ V
57 eqid 2798 . . . . . . 7 (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
5856, 57dmmpti 6465 . . . . . 6 dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)})
5958a1i 11 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
60 1st2nd 7723 . . . . . . . . . . 11 ((Rel 𝐴𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6111, 60sylan 583 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
62 simpr 488 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴)
6361, 62eqeltrrd 2891 . . . . . . . . 9 ((𝜑𝑥𝐴) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
64 df-br 5032 . . . . . . . . 9 ((1st𝑥)𝐴(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
6563, 64sylibr 237 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥)𝐴(2nd𝑥))
6611adantr 484 . . . . . . . . 9 ((𝜑𝑥𝐴) → Rel 𝐴)
67 elrelimasn 5921 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6866, 67syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6965, 68mpbird 260 . . . . . . 7 ((𝜑𝑥𝐴) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
70693ad2antr1 1185 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7170adantr 484 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7211adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → Rel 𝐴)
73 simpr2 1192 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦𝐴)
74 1st2nd 7723 . . . . . . . . . . 11 ((Rel 𝐴𝑦𝐴) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7572, 73, 74syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7675, 73eqeltrrd 2891 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
77 df-br 5032 . . . . . . . . 9 ((1st𝑦)𝐴(2nd𝑦) ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
7876, 77sylibr 237 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦)𝐴(2nd𝑦))
79 elrelimasn 5921 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8072, 79syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8178, 80mpbird 260 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
8281adantr 484 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
83 simpr 488 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (1st𝑥) = (1st𝑦))
8483sneqd 4537 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → {(1st𝑥)} = {(1st𝑦)})
8584imaeq2d 5897 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝐴 “ {(1st𝑥)}) = (𝐴 “ {(1st𝑦)}))
8682, 85eleqtrrd 2893 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
87 simplr3 1214 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝑥𝑦)
88 simpr1 1191 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥𝐴)
8972, 88, 60syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
9089, 75eqeq12d 2814 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩))
91 fvex 6659 . . . . . . . . . 10 (1st𝑥) ∈ V
92 fvex 6659 . . . . . . . . . 10 (2nd𝑥) ∈ V
9391, 92opth 5334 . . . . . . . . 9 (⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦)))
9490, 93syl6bb 290 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦))))
9594baibd 543 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥 = 𝑦 ↔ (2nd𝑥) = (2nd𝑦)))
9695necon3bid 3031 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥𝑦 ↔ (2nd𝑥) ≠ (2nd𝑦)))
9787, 96mpbid 235 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ≠ (2nd𝑦))
9855, 59, 71, 86, 97, 1dprdcntz 19127 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))))
99 df-ov 7139 . . . . . 6 ((1st𝑥)𝑆(2nd𝑥)) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩)
100 oveq2 7144 . . . . . . . 8 (𝑗 = (2nd𝑥) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑥)))
101100, 57, 56fvmpt3i 6751 . . . . . . 7 ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10270, 101syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10389fveq2d 6650 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
10499, 102, 1033eqtr4a 2859 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
105104adantr 484 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
10683oveq1d 7151 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((1st𝑥)𝑆𝑗) = ((1st𝑦)𝑆𝑗))
10785, 106mpteq12dv 5116 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
108107fveq1d 6648 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)))
109 df-ov 7139 . . . . . . . 8 ((1st𝑦)𝑆(2nd𝑦)) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩)
110 oveq2 7144 . . . . . . . . . 10 (𝑗 = (2nd𝑦) → ((1st𝑦)𝑆𝑗) = ((1st𝑦)𝑆(2nd𝑦)))
111 eqid 2798 . . . . . . . . . 10 (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))
112 ovex 7169 . . . . . . . . . 10 ((1st𝑦)𝑆𝑗) ∈ V
113110, 111, 112fvmpt3i 6751 . . . . . . . . 9 ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11481, 113syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11575fveq2d 6650 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
116109, 114, 1153eqtr4a 2859 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
117116adantr 484 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
118108, 117eqtrd 2833 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
119118fveq2d 6650 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))) = ((Cntz‘𝐺)‘(𝑆𝑦)))
12098, 105, 1193sstr3d 3961 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
12111, 41, 12, 29, 4, 3dprd2dlem2 19159 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12245oveq2d 7152 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
123122, 17, 16fvmpt3i 6751 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12452, 123syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
125121, 124sseqtrrd 3956 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1261253ad2antr1 1185 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
127126adantr 484 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1284ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
12918a1i 11 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
130523ad2antr1 1185 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑥) ∈ 𝐼)
131130adantr 484 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ∈ 𝐼)
13212adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom 𝐴𝐼)
133 1stdm 7724 . . . . . . . . 9 ((Rel 𝐴𝑦𝐴) → (1st𝑦) ∈ dom 𝐴)
13472, 73, 133syl2anc 587 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ dom 𝐴)
135132, 134sseldd 3916 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ 𝐼)
136135adantr 484 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑦) ∈ 𝐼)
137 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ≠ (1st𝑦))
138128, 129, 131, 136, 137, 1dprdcntz 19127 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))))
139 sneq 4535 . . . . . . . . . . . . 13 (𝑖 = (1st𝑦) → {𝑖} = {(1st𝑦)})
140139imaeq2d 5897 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑦)}))
141 oveq1 7143 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝑖𝑆𝑗) = ((1st𝑦)𝑆𝑗))
142140, 141mpteq12dv 5116 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
143142oveq2d 7152 . . . . . . . . . 10 (𝑖 = (1st𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
144143, 17, 16fvmpt3i 6751 . . . . . . . . 9 ((1st𝑦) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
145135, 144syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
146145fveq2d 6650 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))))
147 eqid 2798 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
148147dprdssv 19135 . . . . . . . 8 (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
149142breq2d 5043 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
15047adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151149, 150, 135rspcdva 3573 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
152112, 111dmmpti 6465 . . . . . . . . . . 11 dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)})
153152a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)}))
154151, 153, 81dprdub 19144 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
155116, 154eqsstrrd 3954 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
156147, 1cntz2ss 18459 . . . . . . . 8 (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
157148, 155, 156sylancr 590 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
158146, 157eqsstrd 3953 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
159158adantr 484 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
160138, 159sstrd 3925 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
161127, 160sstrd 3925 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
162120, 161pm2.61dane 3074 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
1636adantr 484 . . . . . 6 ((𝜑𝑥𝐴) → 𝐺 ∈ Grp)
164147subgacs 18309 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
165 acsmre 16918 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
166163, 164, 1653syl 18 . . . . 5 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
16714adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = 𝐴)
168 undif2 4383 . . . . . . . . . . . . . . . . . 18 ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})) = ({(1st𝑥)} ∪ 𝐼)
16952snssd 4702 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → {(1st𝑥)} ⊆ 𝐼)
170 ssequn1 4107 . . . . . . . . . . . . . . . . . . 19 ({(1st𝑥)} ⊆ 𝐼 ↔ ({(1st𝑥)} ∪ 𝐼) = 𝐼)
171169, 170sylib 221 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∪ 𝐼) = 𝐼)
172168, 171syl5req 2846 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐼 = ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})))
173172reseq2d 5819 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
174167, 173eqtr3d 2835 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐴 = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
175 resundi 5833 . . . . . . . . . . . . . . 15 (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))) = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
176174, 175eqtrdi 2849 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
177176difeq1d 4049 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}))
178 difundir 4207 . . . . . . . . . . . . 13 (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
179177, 178eqtrdi 2849 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})))
180 neirr 2996 . . . . . . . . . . . . . . . . 17 ¬ (1st𝑥) ≠ (1st𝑥)
18161eleq1d 2874 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
182 df-br 5032 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
18392brresi 5828 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) ∧ (1st𝑥)𝐴(2nd𝑥)))
184183simplbi 501 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}))
185 eldifsni 4683 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) → (1st𝑥) ≠ (1st𝑥))
186184, 185syl 17 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ≠ (1st𝑥))
187182, 186sylbir 238 . . . . . . . . . . . . . . . . . 18 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥))
188181, 187syl6bi 256 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥)))
189180, 188mtoi 202 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
190 disjsn 4607 . . . . . . . . . . . . . . . 16 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
191189, 190sylibr 237 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅)
192 disj3 4361 . . . . . . . . . . . . . . 15 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
193191, 192sylib 221 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
194193eqcomd 2804 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
195194uneq2d 4090 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
196179, 195eqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
197196imaeq2d 5897 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
198 imaundi 5976 . . . . . . . . . 10 (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
199197, 198eqtrdi 2849 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
200199unieqd 4815 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
201 uniun 4824 . . . . . . . 8 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
202200, 201eqtrdi 2849 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
203 imassrn 5908 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
20441frnd 6495 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
205204adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
206 mresspw 16858 . . . . . . . . . . . . 13 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
207166, 206syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
208205, 207sstrd 3925 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
209203, 208sstrid 3926 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
210 sspwuni 4986 . . . . . . . . . 10 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
211209, 210sylib 221 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
212166, 3, 211mrcssidd 16891 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
213 imassrn 5908 . . . . . . . . . . 11 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ ran 𝑆
214213, 208sstrid 3926 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
215 sspwuni 4986 . . . . . . . . . 10 ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
216214, 215sylib 221 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
217166, 3, 216mrcssidd 16891 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
218 unss12 4109 . . . . . . . 8 (( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
219212, 217, 218syl2anc 587 . . . . . . 7 ((𝜑𝑥𝐴) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
220202, 219eqsstrd 3953 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
2213mrccl 16877 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
222166, 211, 221syl2anc 587 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
2233mrccl 16877 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
224166, 216, 223syl2anc 587 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
225 eqid 2798 . . . . . . . 8 (LSSum‘𝐺) = (LSSum‘𝐺)
226225lsmunss 18780 . . . . . . 7 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
227222, 224, 226syl2anc 587 . . . . . 6 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
228220, 227sstrd 3925 . . . . 5 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
229 difss 4059 . . . . . . . . . . . . 13 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st𝑥)})
230 ressn 6105 . . . . . . . . . . . . 13 (𝐴 ↾ {(1st𝑥)}) = ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
231229, 230sseqtri 3951 . . . . . . . . . . . 12 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
232 imass2 5933 . . . . . . . . . . . 12 (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))))
233231, 232ax-mp 5 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
234 ovex 7169 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝑆𝑖) ∈ V
235 oveq2 7144 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆𝑖))
23657, 235elrnmpt1s 5794 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝐴 “ {(1st𝑥)}) ∧ ((1st𝑥)𝑆𝑖) ∈ V) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
237234, 236mpan2 690 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝐴 “ {(1st𝑥)}) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
238237rgen 3116 . . . . . . . . . . . . . 14 𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
239238a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
240 oveq1 7143 . . . . . . . . . . . . . . . 16 (𝑦 = (1st𝑥) → (𝑦𝑆𝑖) = ((1st𝑥)𝑆𝑖))
241240eleq1d 2874 . . . . . . . . . . . . . . 15 (𝑦 = (1st𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
242241ralbidv 3162 . . . . . . . . . . . . . 14 (𝑦 = (1st𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
24391, 242ralsn 4579 . . . . . . . . . . . . 13 (∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
244239, 243sylibr 237 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
24541adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
246245ffund 6492 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun 𝑆)
247 resss 5844 . . . . . . . . . . . . . . 15 (𝐴 ↾ {(1st𝑥)}) ⊆ 𝐴
248230, 247eqsstrri 3950 . . . . . . . . . . . . . 14 ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ 𝐴
249245fdmd 6498 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → dom 𝑆 = 𝐴)
250248, 249sseqtrrid 3968 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆)
251 funimassov 7307 . . . . . . . . . . . . 13 ((Fun 𝑆 ∧ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
252246, 250, 251syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
253244, 252mpbird 260 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
254233, 253sstrid 3926 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
255254unissd 4811 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
256 df-ov 7139 . . . . . . . . . . . . . 14 ((1st𝑥)𝑆𝑗) = (𝑆‘⟨(1st𝑥), 𝑗⟩)
25741ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
258 elrelimasn 5921 . . . . . . . . . . . . . . . . . 18 (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
25966, 258syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
260259biimpa 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (1st𝑥)𝐴𝑗)
261 df-br 5032 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝐴𝑗 ↔ ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
262260, 261sylib 221 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
263257, 262ffvelrnd 6830 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (𝑆‘⟨(1st𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
264256, 263eqeltrid 2894 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ((1st𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
265264fmpttd 6857 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺))
266265frnd 6495 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
267266, 207sstrd 3925 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
268 sspwuni 4986 . . . . . . . . . 10 (ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
269267, 268sylib 221 . . . . . . . . 9 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
270166, 3, 255, 269mrcssd 16890 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2713dprdspan 19146 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27253, 271syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
273270, 272sseqtrrd 3956 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27416, 17fnmpti 6464 . . . . . . . . . . . . 13 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
275 fnressn 6898 . . . . . . . . . . . . 13 (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st𝑥) ∈ 𝐼) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
276274, 52, 275sylancr 590 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
277124opeq2d 4773 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩ = ⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩)
278277sneqd 4537 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩} = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
279276, 278eqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
280279oveq2d 7152 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}))
281 dprdsubg 19143 . . . . . . . . . . . . 13 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
28253, 281syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
283 dprdsn 19155 . . . . . . . . . . . 12 (((1st𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
28452, 282, 283syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
285284simprd 499 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
286280, 285eqtrd 2833 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2874adantr 484 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
28818a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
289 difss 4059 . . . . . . . . . . 11 (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼
290289a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼)
291 disjdif 4379 . . . . . . . . . . 11 ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅
292291a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅)
293287, 288, 169, 290, 292, 1dprdcntz2 19157 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
294286, 293eqsstrrd 3954 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
29529adantlr 714 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
29666, 245, 49, 295, 287, 3, 290dprd2dlem1 19160 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
297 resmpt 5873 . . . . . . . . . . . 12 ((𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
298289, 297ax-mp 5 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
299298oveq2i 7147 . . . . . . . . . 10 (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
300296, 299eqtr4di 2851 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
301300fveq2d 6650 . . . . . . . 8 ((𝜑𝑥𝐴) → ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
302294, 301sseqtrrd 3956 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
303273, 302sstrd 3925 . . . . . 6 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
304225, 1lsmsubg 18775 . . . . . 6 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
305222, 224, 303, 304syl3anc 1368 . . . . 5 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
3063mrcsscl 16886 . . . . 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 4161 . . . 4 ((𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
309307, 308syl 17 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
31041ffvelrnda 6829 . . . 4 ((𝜑𝑥𝐴) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
311225lsmlub 18786 . . . . . . . . . 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 711 . . . . . . . 8 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
314313, 124sseqtrrd 3956 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
315287, 288, 290dprdres 19147 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) ∧ (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
316315simpld 498 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
3173dprdspan 19146 . . . . . . . . . . 11 (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
318316, 317syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
319 df-ima 5533 . . . . . . . . . . . 12 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
320319unieqi 4814 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
321320fveq2i 6649 . . . . . . . . . 10 (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
322318, 321eqtr4di 2851 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
323300, 322eqtrd 2833 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
324 eqimss 3971 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
325323, 324syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
326 ss2in 4163 . . . . . . 7 ((((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
327314, 325, 326syl2anc 587 . . . . . 6 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
328287, 288, 52, 2, 3dprddisj 19128 . . . . . 6 ((𝜑𝑥𝐴) → (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) = {(0g𝐺)})
329327, 328sseqtrd 3955 . . . . 5 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ {(0g𝐺)})
330225lsmub2 18779 . . . . . . . . 9 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺)) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
331222, 310, 330syl2anc 587 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3322subg0cl 18283 . . . . . . . . 9 ((𝑆𝑥) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑆𝑥))
333310, 332syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝑆𝑥))
334331, 333sseldd 3916 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3352subg0cl 18283 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
336224, 335syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
337334, 336elind 4121 . . . . . 6 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
338337snssd 4702 . . . . 5 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
339329, 338eqssd 3932 . . . 4 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = {(0g𝐺)})
340 incom 4128 . . . . 5 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
34169, 101syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
34261fveq2d 6650 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
34399, 341, 3423eqtr4a 2859 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
344 eqimss2 3972 . . . . . . . . 9 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
345343, 344syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
346 eldifsn 4680 . . . . . . . . . . . . 13 (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥))
34711ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → Rel 𝐴)
348 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st𝑥)}))
349247, 348sseldi 3913 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝐴)
350347, 349, 74syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
351350fveq2d 6650 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
352351, 109eqtr4di 2851 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑦)𝑆(2nd𝑦)))
353350, 348eqeltrrd 2891 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}))
354 fvex 6659 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑦) ∈ V
355354opelresi 5827 . . . . . . . . . . . . . . . . . . . . 21 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) ↔ ((1st𝑦) ∈ {(1st𝑥)} ∧ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴))
356355simplbi 501 . . . . . . . . . . . . . . . . . . . 20 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) → (1st𝑦) ∈ {(1st𝑥)})
357353, 356syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) ∈ {(1st𝑥)})
358 elsni 4542 . . . . . . . . . . . . . . . . . . 19 ((1st𝑦) ∈ {(1st𝑥)} → (1st𝑦) = (1st𝑥))
359357, 358syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) = (1st𝑥))
360359oveq1d 7151 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑦)𝑆(2nd𝑦)) = ((1st𝑥)𝑆(2nd𝑦)))
361352, 360eqtrd 2833 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑥)𝑆(2nd𝑦)))
362348, 230eleqtrdi 2900 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
363 xp2nd 7707 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
364362, 363syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
365 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝑥)
36661adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
367350, 366eqeq12d 2814 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩))
368 fvex 6659 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑦) ∈ V
369368, 354opth 5334 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ ((1st𝑦) = (1st𝑥) ∧ (2nd𝑦) = (2nd𝑥)))
370369baib 539 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑦) = (1st𝑥) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
371359, 370syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
372367, 371bitrd 282 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ (2nd𝑦) = (2nd𝑥)))
373372necon3bid 3031 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦𝑥 ↔ (2nd𝑦) ≠ (2nd𝑥)))
374365, 373mpbid 235 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ≠ (2nd𝑥))
375 eldifsn 4680 . . . . . . . . . . . . . . . . . 18 ((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↔ ((2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}) ∧ (2nd𝑦) ≠ (2nd𝑥)))
376364, 374, 375sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
377 ovex 7169 . . . . . . . . . . . . . . . . 17 ((1st𝑥)𝑆(2nd𝑦)) ∈ V
378 difss 4059 . . . . . . . . . . . . . . . . . . 19 ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)})
379 resmpt 5873 . . . . . . . . . . . . . . . . . . 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 7144 . . . . . . . . . . . . . . . . . 18 (𝑗 = (2nd𝑦) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑦)))
382380, 381elrnmpt1s 5794 . . . . . . . . . . . . . . . . 17 (((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ∧ ((1st𝑥)𝑆(2nd𝑦)) ∈ V) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
383376, 377, 382sylancl 589 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
384361, 383eqeltrd 2890 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
385 df-ima 5533 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
386384, 385eleqtrrdi 2901 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
387386ex 416 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
388346, 387syl5bi 245 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
389388ralrimiv 3148 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
390231, 250sstrid 3926 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
391 funimass4 6706 . . . . . . . . . . . 12 ((Fun 𝑆 ∧ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
392246, 390, 391syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
393389, 392mpbird 260 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
394393unissd 4811 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
395 imassrn 5908 . . . . . . . . . . 11 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
396395, 267sstrid 3926 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺))
397 sspwuni 4986 . . . . . . . . . 10 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
398396, 397sylib 221 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
399166, 3, 394, 398mrcssd 16890 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
400 ss2in 4163 . . . . . . . 8 (((𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
401345, 399, 400syl2anc 587 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
40258a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
40353, 402, 69, 2, 3dprddisj 19128 . . . . . . 7 ((𝜑𝑥𝐴) → (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) = {(0g𝐺)})
404401, 403sseqtrd 3955 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ {(0g𝐺)})
4052subg0cl 18283 . . . . . . . . 9 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
406222, 405syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
407333, 406elind 4121 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
408407snssd 4702 . . . . . 6 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
409404, 408eqssd 3932 . . . . 5 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) = {(0g𝐺)})
410340, 409syl5eq 2845 . . . 4 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = {(0g𝐺)})
411225, 222, 310, 224, 2, 339, 410lsmdisj2 18804 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) = {(0g𝐺)})
412309, 411sseqtrd 3955 . 2 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g𝐺)})
4131, 2, 3, 6, 40, 41, 162, 412dmdprdd 19118 1 (𝜑𝐺dom DProd 𝑆)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ⟨cop 4531  ∪ cuni 4801  ∪ ciun 4882   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  dom cdm 5520  ran crn 5521   ↾ cres 5522   “ cima 5523  Rel wrel 5525  Fun wfun 6319   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136  1st c1st 7672  2nd c2nd 7673  Basecbs 16478  0gc0g 16708  Moorecmre 16848  mrClscmrc 16849  ACScacs 16851  Grpcgrp 18098  SubGrpcsubg 18269  Cntzccntz 18441  LSSumclsm 18755   DProd cdprd 19112 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-om 7564  df-1st 7674  df-2nd 7675  df-supp 7817  df-tpos 7878  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-map 8394  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8821  df-oi 8961  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11629  df-2 11691  df-n0 11889  df-z 11973  df-uz 12235  df-fz 12889  df-fzo 13032  df-seq 13368  df-hash 13690  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-0g 16710  df-gsum 16711  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18101  df-minusg 18102  df-sbg 18103  df-mulg 18221  df-subg 18272  df-ghm 18352  df-gim 18395  df-cntz 18443  df-oppg 18470  df-lsm 18757  df-cmn 18904  df-dprd 19114 This theorem is referenced by:  dprd2db  19162  dprd2d2  19163
 Copyright terms: Public domain W3C validator