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

Theorem dprd2da 18264
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 2610 . 2 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2610 . 2 (0g𝐺) = (0g𝐺)
3 dprd2d.k . 2 𝐾 = (mrCls‘(SubGrp‘𝐺))
4 dprd2d.5 . . 3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5 dprdgrp 18227 . . 3 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
64, 5syl 17 . 2 (𝜑𝐺 ∈ Grp)
7 resiun2 5338 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = 𝑖𝐼 (𝐴 ↾ {𝑖})
8 iunid 4511 . . . . . 6 𝑖𝐼 {𝑖} = 𝐼
98reseq2i 5314 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = (𝐴𝐼)
107, 9eqtr3i 2634 . . . 4 𝑖𝐼 (𝐴 ↾ {𝑖}) = (𝐴𝐼)
11 dprd2d.1 . . . . 5 (𝜑 → Rel 𝐴)
12 dprd2d.3 . . . . 5 (𝜑 → dom 𝐴𝐼)
13 relssres 5357 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝐼) → (𝐴𝐼) = 𝐴)
1411, 12, 13syl2anc 691 . . . 4 (𝜑 → (𝐴𝐼) = 𝐴)
1510, 14syl5eq 2656 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16 ovex 6577 . . . . . 6 (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17 eqid 2610 . . . . . 6 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
1816, 17dmmpti 5936 . . . . 5 dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19 reldmdprd 18219 . . . . . . 7 Rel dom DProd
2019brrelex2i 5083 . . . . . 6 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21 dmexg 6989 . . . . . 6 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
224, 20, 213syl 18 . . . . 5 (𝜑 → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
2318, 22syl5eqelr 2693 . . . 4 (𝜑𝐼 ∈ V)
24 ressn 5588 . . . . . 6 (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25 snex 4835 . . . . . . 7 {𝑖} ∈ V
26 ovex 6577 . . . . . . . . 9 (𝑖𝑆𝑗) ∈ V
27 eqid 2610 . . . . . . . . 9 (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
2826, 27dmmpti 5936 . . . . . . . 8 dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29 dprd2d.4 . . . . . . . . 9 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
3019brrelex2i 5083 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31 dmexg 6989 . . . . . . . . 9 ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3229, 30, 313syl 18 . . . . . . . 8 ((𝜑𝑖𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3328, 32syl5eqelr 2693 . . . . . . 7 ((𝜑𝑖𝐼) → (𝐴 “ {𝑖}) ∈ V)
34 xpexg 6858 . . . . . . 7 (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3525, 33, 34sylancr 694 . . . . . 6 ((𝜑𝑖𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3624, 35syl5eqel 2692 . . . . 5 ((𝜑𝑖𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
3736ralrimiva 2949 . . . 4 (𝜑 → ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38 iunexg 7035 . . . 4 ((𝐼 ∈ V ∧ ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V) → 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
3923, 37, 38syl2anc 691 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
4015, 39eqeltrrd 2689 . 2 (𝜑𝐴 ∈ V)
41 dprd2d.2 . 2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
4212adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐴) → dom 𝐴𝐼)
43 1stdm 7106 . . . . . . . . . 10 ((Rel 𝐴𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
4411, 43sylan 487 . . . . . . . . 9 ((𝜑𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
4542, 44sseldd 3569 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥) ∈ 𝐼)
4629ralrimiva 2949 . . . . . . . . 9 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4746adantr 480 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48 sneq 4135 . . . . . . . . . . . 12 (𝑖 = (1st𝑥) → {𝑖} = {(1st𝑥)})
4948imaeq2d 5385 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑥)}))
50 oveq1 6556 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → (𝑖𝑆𝑗) = ((1st𝑥)𝑆𝑗))
5149, 50mpteq12dv 4663 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5251breq2d 4595 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
5352rspcv 3278 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
5445, 47, 53sylc 63 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
55543ad2antr1 1219 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5655adantr 480 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
57 ovex 6577 . . . . . . 7 ((1st𝑥)𝑆𝑗) ∈ V
58 eqid 2610 . . . . . . 7 (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
5957, 58dmmpti 5936 . . . . . 6 dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)})
6059a1i 11 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
61 1st2nd 7105 . . . . . . . . . . 11 ((Rel 𝐴𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6211, 61sylan 487 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
63 simpr 476 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴)
6462, 63eqeltrrd 2689 . . . . . . . . 9 ((𝜑𝑥𝐴) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
65 df-br 4584 . . . . . . . . 9 ((1st𝑥)𝐴(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
6664, 65sylibr 223 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥)𝐴(2nd𝑥))
6711adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐴) → Rel 𝐴)
68 elrelimasn 5408 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6967, 68syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
7066, 69mpbird 246 . . . . . . 7 ((𝜑𝑥𝐴) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
71703ad2antr1 1219 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7271adantr 480 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7311adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → Rel 𝐴)
74 simpr2 1061 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦𝐴)
75 1st2nd 7105 . . . . . . . . . . 11 ((Rel 𝐴𝑦𝐴) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7673, 74, 75syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7776, 74eqeltrrd 2689 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
78 df-br 4584 . . . . . . . . 9 ((1st𝑦)𝐴(2nd𝑦) ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
7977, 78sylibr 223 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦)𝐴(2nd𝑦))
80 elrelimasn 5408 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8173, 80syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8279, 81mpbird 246 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
8382adantr 480 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
84 simpr 476 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (1st𝑥) = (1st𝑦))
8584sneqd 4137 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → {(1st𝑥)} = {(1st𝑦)})
8685imaeq2d 5385 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝐴 “ {(1st𝑥)}) = (𝐴 “ {(1st𝑦)}))
8783, 86eleqtrrd 2691 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
88 simplr3 1098 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝑥𝑦)
89 simpr1 1060 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥𝐴)
9073, 89, 61syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
9190, 76eqeq12d 2625 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩))
92 fvex 6113 . . . . . . . . . 10 (1st𝑥) ∈ V
93 fvex 6113 . . . . . . . . . 10 (2nd𝑥) ∈ V
9492, 93opth 4871 . . . . . . . . 9 (⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦)))
9591, 94syl6bb 275 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦))))
9695baibd 946 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥 = 𝑦 ↔ (2nd𝑥) = (2nd𝑦)))
9796necon3bid 2826 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥𝑦 ↔ (2nd𝑥) ≠ (2nd𝑦)))
9888, 97mpbid 221 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ≠ (2nd𝑦))
9956, 60, 72, 87, 98, 1dprdcntz 18230 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))))
100 df-ov 6552 . . . . . 6 ((1st𝑥)𝑆(2nd𝑥)) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩)
101 oveq2 6557 . . . . . . . 8 (𝑗 = (2nd𝑥) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑥)))
102101, 58, 57fvmpt3i 6196 . . . . . . 7 ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10371, 102syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10490fveq2d 6107 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
105100, 103, 1043eqtr4a 2670 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
106105adantr 480 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
10784oveq1d 6564 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((1st𝑥)𝑆𝑗) = ((1st𝑦)𝑆𝑗))
10886, 107mpteq12dv 4663 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
109108fveq1d 6105 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)))
110 df-ov 6552 . . . . . . . 8 ((1st𝑦)𝑆(2nd𝑦)) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩)
111 oveq2 6557 . . . . . . . . . 10 (𝑗 = (2nd𝑦) → ((1st𝑦)𝑆𝑗) = ((1st𝑦)𝑆(2nd𝑦)))
112 eqid 2610 . . . . . . . . . 10 (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))
113 ovex 6577 . . . . . . . . . 10 ((1st𝑦)𝑆𝑗) ∈ V
114111, 112, 113fvmpt3i 6196 . . . . . . . . 9 ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11582, 114syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11676fveq2d 6107 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
117110, 115, 1163eqtr4a 2670 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
118117adantr 480 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
119109, 118eqtrd 2644 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
120119fveq2d 6107 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))) = ((Cntz‘𝐺)‘(𝑆𝑦)))
12199, 106, 1203sstr3d 3610 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
12211, 41, 12, 29, 4, 3dprd2dlem2 18262 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12351oveq2d 6565 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
124123, 17, 16fvmpt3i 6196 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12545, 124syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
126122, 125sseqtr4d 3605 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1271263ad2antr1 1219 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
128127adantr 480 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1294ad2antrr 758 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
13018a1i 11 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
131453ad2antr1 1219 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑥) ∈ 𝐼)
132131adantr 480 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ∈ 𝐼)
13312adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom 𝐴𝐼)
134 1stdm 7106 . . . . . . . . 9 ((Rel 𝐴𝑦𝐴) → (1st𝑦) ∈ dom 𝐴)
13573, 74, 134syl2anc 691 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ dom 𝐴)
136133, 135sseldd 3569 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ 𝐼)
137136adantr 480 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑦) ∈ 𝐼)
138 simpr 476 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ≠ (1st𝑦))
139129, 130, 132, 137, 138, 1dprdcntz 18230 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))))
140 sneq 4135 . . . . . . . . . . . . 13 (𝑖 = (1st𝑦) → {𝑖} = {(1st𝑦)})
141140imaeq2d 5385 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑦)}))
142 oveq1 6556 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝑖𝑆𝑗) = ((1st𝑦)𝑆𝑗))
143141, 142mpteq12dv 4663 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
144143oveq2d 6565 . . . . . . . . . 10 (𝑖 = (1st𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
145144, 17, 16fvmpt3i 6196 . . . . . . . . 9 ((1st𝑦) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
146136, 145syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
147146fveq2d 6107 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))))
148 eqid 2610 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
149148dprdssv 18238 . . . . . . . 8 (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
15046adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151143breq2d 4595 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
152151rspcv 3278 . . . . . . . . . . 11 ((1st𝑦) ∈ 𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
153136, 150, 152sylc 63 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
154113, 112dmmpti 5936 . . . . . . . . . . 11 dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)})
155154a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)}))
156153, 155, 82dprdub 18247 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
157117, 156eqsstr3d 3603 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
158148, 1cntz2ss 17588 . . . . . . . 8 (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
159149, 157, 158sylancr 694 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
160147, 159eqsstrd 3602 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
161160adantr 480 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
162139, 161sstrd 3578 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
163128, 162sstrd 3578 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
164121, 163pm2.61dane 2869 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
1656adantr 480 . . . . . 6 ((𝜑𝑥𝐴) → 𝐺 ∈ Grp)
166148subgacs 17452 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
167 acsmre 16136 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
168165, 166, 1673syl 18 . . . . 5 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
16914adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = 𝐴)
170 undif2 3996 . . . . . . . . . . . . . . . . . 18 ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})) = ({(1st𝑥)} ∪ 𝐼)
17145snssd 4281 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → {(1st𝑥)} ⊆ 𝐼)
172 ssequn1 3745 . . . . . . . . . . . . . . . . . . 19 ({(1st𝑥)} ⊆ 𝐼 ↔ ({(1st𝑥)} ∪ 𝐼) = 𝐼)
173171, 172sylib 207 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∪ 𝐼) = 𝐼)
174170, 173syl5req 2657 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐼 = ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})))
175174reseq2d 5317 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
176169, 175eqtr3d 2646 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐴 = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
177 resundi 5330 . . . . . . . . . . . . . . 15 (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))) = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
178176, 177syl6eq 2660 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
179178difeq1d 3689 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}))
180 difundir 3839 . . . . . . . . . . . . 13 (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
181179, 180syl6eq 2660 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})))
182 neirr 2791 . . . . . . . . . . . . . . . . 17 ¬ (1st𝑥) ≠ (1st𝑥)
18362eleq1d 2672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
184 df-br 4584 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
18593brres 5323 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ((1st𝑥)𝐴(2nd𝑥) ∧ (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)})))
186185simprbi 479 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}))
187 eldifsni 4261 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) → (1st𝑥) ≠ (1st𝑥))
188186, 187syl 17 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ≠ (1st𝑥))
189184, 188sylbir 224 . . . . . . . . . . . . . . . . . 18 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥))
190183, 189syl6bi 242 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥)))
191182, 190mtoi 189 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
192 disjsn 4192 . . . . . . . . . . . . . . . 16 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
193191, 192sylibr 223 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅)
194 disj3 3973 . . . . . . . . . . . . . . 15 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
195193, 194sylib 207 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
196195eqcomd 2616 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
197196uneq2d 3729 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
198181, 197eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
199198imaeq2d 5385 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
200 imaundi 5464 . . . . . . . . . 10 (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
201199, 200syl6eq 2660 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
202201unieqd 4382 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
203 uniun 4392 . . . . . . . 8 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
204202, 203syl6eq 2660 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
205 imassrn 5396 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
206 frn 5966 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺))
20741, 206syl 17 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
208207adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
209 mresspw 16075 . . . . . . . . . . . . 13 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
210168, 209syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
211208, 210sstrd 3578 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
212205, 211syl5ss 3579 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
213 sspwuni 4547 . . . . . . . . . 10 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
214212, 213sylib 207 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
215168, 3, 214mrcssidd 16108 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
216 imassrn 5396 . . . . . . . . . . 11 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ ran 𝑆
217216, 211syl5ss 3579 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
218 sspwuni 4547 . . . . . . . . . 10 ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
219217, 218sylib 207 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
220168, 3, 219mrcssidd 16108 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
221 unss12 3747 . . . . . . . 8 (( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
222215, 220, 221syl2anc 691 . . . . . . 7 ((𝜑𝑥𝐴) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
223204, 222eqsstrd 3602 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
2243mrccl 16094 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
225168, 214, 224syl2anc 691 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
2263mrccl 16094 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
227168, 219, 226syl2anc 691 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
228 eqid 2610 . . . . . . . 8 (LSSum‘𝐺) = (LSSum‘𝐺)
229228lsmunss 17896 . . . . . . 7 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
230225, 227, 229syl2anc 691 . . . . . 6 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
231223, 230sstrd 3578 . . . . 5 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
232 difss 3699 . . . . . . . . . . . . 13 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st𝑥)})
233 ressn 5588 . . . . . . . . . . . . 13 (𝐴 ↾ {(1st𝑥)}) = ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
234232, 233sseqtri 3600 . . . . . . . . . . . 12 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
235 imass2 5420 . . . . . . . . . . . 12 (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))))
236234, 235ax-mp 5 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
237 ovex 6577 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝑆𝑖) ∈ V
238 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆𝑖))
23958, 238elrnmpt1s 5294 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝐴 “ {(1st𝑥)}) ∧ ((1st𝑥)𝑆𝑖) ∈ V) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
240237, 239mpan2 703 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝐴 “ {(1st𝑥)}) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
241240rgen 2906 . . . . . . . . . . . . . 14 𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
242241a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
243 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑦 = (1st𝑥) → (𝑦𝑆𝑖) = ((1st𝑥)𝑆𝑖))
244243eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑦 = (1st𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
245244ralbidv 2969 . . . . . . . . . . . . . 14 (𝑦 = (1st𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
24692, 245ralsn 4169 . . . . . . . . . . . . 13 (∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
247242, 246sylibr 223 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
24841adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
249 ffun 5961 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆)
250248, 249syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun 𝑆)
251 resss 5342 . . . . . . . . . . . . . . 15 (𝐴 ↾ {(1st𝑥)}) ⊆ 𝐴
252233, 251eqsstr3i 3599 . . . . . . . . . . . . . 14 ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ 𝐴
253 fdm 5964 . . . . . . . . . . . . . . 15 (𝑆:𝐴⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐴)
254248, 253syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → dom 𝑆 = 𝐴)
255252, 254syl5sseqr 3617 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆)
256 funimassov 6709 . . . . . . . . . . . . 13 ((Fun 𝑆 ∧ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
257250, 255, 256syl2anc 691 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
258247, 257mpbird 246 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
259236, 258syl5ss 3579 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
260259unissd 4398 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
261 df-ov 6552 . . . . . . . . . . . . . 14 ((1st𝑥)𝑆𝑗) = (𝑆‘⟨(1st𝑥), 𝑗⟩)
26241ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
263 elrelimasn 5408 . . . . . . . . . . . . . . . . . 18 (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
26467, 263syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
265264biimpa 500 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (1st𝑥)𝐴𝑗)
266 df-br 4584 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝐴𝑗 ↔ ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
267265, 266sylib 207 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
268262, 267ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (𝑆‘⟨(1st𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
269261, 268syl5eqel 2692 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ((1st𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
270269, 58fmptd 6292 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺))
271 frn 5966 . . . . . . . . . . . 12 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
272270, 271syl 17 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
273272, 210sstrd 3578 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
274 sspwuni 4547 . . . . . . . . . 10 (ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
275273, 274sylib 207 . . . . . . . . 9 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
276168, 3, 260, 275mrcssd 16107 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2773dprdspan 18249 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27854, 277syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
279276, 278sseqtr4d 3605 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
28016, 17fnmpti 5935 . . . . . . . . . . . . 13 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
281 fnressn 6330 . . . . . . . . . . . . 13 (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st𝑥) ∈ 𝐼) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
282280, 45, 281sylancr 694 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
283125opeq2d 4347 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩ = ⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩)
284283sneqd 4137 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩} = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
285282, 284eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
286285oveq2d 6565 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}))
287 dprdsubg 18246 . . . . . . . . . . . . 13 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
28854, 287syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
289 dprdsn 18258 . . . . . . . . . . . 12 (((1st𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
29045, 288, 289syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
291290simprd 478 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
292286, 291eqtrd 2644 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2934adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
29418a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
295 difss 3699 . . . . . . . . . . 11 (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼
296295a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼)
297 disjdif 3992 . . . . . . . . . . 11 ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅
298297a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅)
299293, 294, 171, 296, 298, 1dprdcntz2 18260 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
300292, 299eqsstr3d 3603 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
30129adantlr 747 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30267, 248, 42, 301, 293, 3, 296dprd2dlem1 18263 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
303 resmpt 5369 . . . . . . . . . . . 12 ((𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
304295, 303ax-mp 5 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
305304oveq2i 6560 . . . . . . . . . 10 (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
306302, 305syl6eqr 2662 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
307306fveq2d 6107 . . . . . . . 8 ((𝜑𝑥𝐴) → ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
308300, 307sseqtr4d 3605 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
309279, 308sstrd 3578 . . . . . 6 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
310228, 1lsmsubg 17892 . . . . . 6 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
311225, 227, 309, 310syl3anc 1318 . . . . 5 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
3123mrcsscl 16103 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∧ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
313168, 231, 311, 312syl3anc 1318 . . . 4 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
314 sslin 3801 . . . 4 ((𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
315313, 314syl 17 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
31641ffvelrnda 6267 . . . 4 ((𝜑𝑥𝐴) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
317228lsmlub 17901 . . . . . . . . . 10 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
318225, 316, 288, 317syl3anc 1318 . . . . . . . . 9 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
319279, 122, 318mpbi2and 958 . . . . . . . 8 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
320319, 125sseqtr4d 3605 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
321293, 294, 296dprdres 18250 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) ∧ (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
322321simpld 474 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
3233dprdspan 18249 . . . . . . . . . . 11 (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
324322, 323syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
325 df-ima 5051 . . . . . . . . . . . 12 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
326325unieqi 4381 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
327326fveq2i 6106 . . . . . . . . . 10 (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
328324, 327syl6eqr 2662 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
329306, 328eqtrd 2644 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
330 eqimss 3620 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
331329, 330syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
332 ss2in 3802 . . . . . . 7 ((((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
333320, 331, 332syl2anc 691 . . . . . 6 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
334293, 294, 45, 2, 3dprddisj 18231 . . . . . 6 ((𝜑𝑥𝐴) → (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) = {(0g𝐺)})
335333, 334sseqtrd 3604 . . . . 5 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ {(0g𝐺)})
336228lsmub2 17895 . . . . . . . . 9 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺)) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
337225, 316, 336syl2anc 691 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3382subg0cl 17425 . . . . . . . . 9 ((𝑆𝑥) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑆𝑥))
339316, 338syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝑆𝑥))
340337, 339sseldd 3569 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3412subg0cl 17425 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
342227, 341syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
343340, 342elind 3760 . . . . . 6 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
344343snssd 4281 . . . . 5 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
345335, 344eqssd 3585 . . . 4 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = {(0g𝐺)})
346 incom 3767 . . . . 5 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
34770, 102syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
34862fveq2d 6107 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
349100, 347, 3483eqtr4a 2670 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
350 eqimss2 3621 . . . . . . . . 9 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
351349, 350syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
352 eldifsn 4260 . . . . . . . . . . . . 13 (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥))
35311ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → Rel 𝐴)
354 simprl 790 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st𝑥)}))
355251, 354sseldi 3566 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝐴)
356353, 355, 75syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
357356fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
358357, 110syl6eqr 2662 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑦)𝑆(2nd𝑦)))
359356, 354eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}))
360 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑦) ∈ V
361360opelres 5322 . . . . . . . . . . . . . . . . . . . . 21 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) ↔ (⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴 ∧ (1st𝑦) ∈ {(1st𝑥)}))
362361simprbi 479 . . . . . . . . . . . . . . . . . . . 20 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) → (1st𝑦) ∈ {(1st𝑥)})
363359, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) ∈ {(1st𝑥)})
364 elsni 4142 . . . . . . . . . . . . . . . . . . 19 ((1st𝑦) ∈ {(1st𝑥)} → (1st𝑦) = (1st𝑥))
365363, 364syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) = (1st𝑥))
366365oveq1d 6564 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑦)𝑆(2nd𝑦)) = ((1st𝑥)𝑆(2nd𝑦)))
367358, 366eqtrd 2644 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑥)𝑆(2nd𝑦)))
368354, 233syl6eleq 2698 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
369 xp2nd 7090 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
370368, 369syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
371 simprr 792 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝑥)
37262adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
373356, 372eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩))
374 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑦) ∈ V
375374, 360opth 4871 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ ((1st𝑦) = (1st𝑥) ∧ (2nd𝑦) = (2nd𝑥)))
376375baib 942 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑦) = (1st𝑥) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
377365, 376syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
378373, 377bitrd 267 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ (2nd𝑦) = (2nd𝑥)))
379378necon3bid 2826 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦𝑥 ↔ (2nd𝑦) ≠ (2nd𝑥)))
380371, 379mpbid 221 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ≠ (2nd𝑥))
381 eldifsn 4260 . . . . . . . . . . . . . . . . . 18 ((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↔ ((2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}) ∧ (2nd𝑦) ≠ (2nd𝑥)))
382370, 380, 381sylanbrc 695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
383 ovex 6577 . . . . . . . . . . . . . . . . 17 ((1st𝑥)𝑆(2nd𝑦)) ∈ V
384 difss 3699 . . . . . . . . . . . . . . . . . . 19 ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)})
385 resmpt 5369 . . . . . . . . . . . . . . . . . . 19 (((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
386384, 385ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
387 oveq2 6557 . . . . . . . . . . . . . . . . . 18 (𝑗 = (2nd𝑦) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑦)))
388386, 387elrnmpt1s 5294 . . . . . . . . . . . . . . . . 17 (((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ∧ ((1st𝑥)𝑆(2nd𝑦)) ∈ V) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
389382, 383, 388sylancl 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑥)𝑆(2nd𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
390367, 389eqeltrd 2688 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
391 df-ima 5051 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
392390, 391syl6eleqr 2699 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
393392ex 449 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
394352, 393syl5bi 231 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
395394ralrimiv 2948 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
396234, 255syl5ss 3579 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
397 funimass4 6157 . . . . . . . . . . . 12 ((Fun 𝑆 ∧ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
398250, 396, 397syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
399395, 398mpbird 246 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
400399unissd 4398 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
401 imassrn 5396 . . . . . . . . . . 11 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
402401, 273syl5ss 3579 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺))
403 sspwuni 4547 . . . . . . . . . 10 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
404402, 403sylib 207 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
405168, 3, 400, 404mrcssd 16107 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
406 ss2in 3802 . . . . . . . 8 (((𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
407351, 405, 406syl2anc 691 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
40859a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
40954, 408, 70, 2, 3dprddisj 18231 . . . . . . 7 ((𝜑𝑥𝐴) → (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) = {(0g𝐺)})
410407, 409sseqtrd 3604 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ {(0g𝐺)})
4112subg0cl 17425 . . . . . . . . 9 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
412225, 411syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
413339, 412elind 3760 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
414413snssd 4281 . . . . . 6 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
415410, 414eqssd 3585 . . . . 5 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) = {(0g𝐺)})
416346, 415syl5eq 2656 . . . 4 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = {(0g𝐺)})
417228, 225, 316, 227, 2, 345, 416lsmdisj2 17918 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) = {(0g𝐺)})
418315, 417sseqtrd 3604 . 2 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g𝐺)})
4191, 2, 3, 6, 40, 41, 164, 418dmdprdd 18221 1 (𝜑𝐺dom DProd 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  Vcvv 3173  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108  {csn 4125  cop 4131   cuni 4372   ciun 4455   class class class wbr 4583  cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  cres 5040  cima 5041  Rel wrel 5043  Fun wfun 5798   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058  Basecbs 15695  0gc0g 15923  Moorecmre 16065  mrClscmrc 16066  ACScacs 16068  Grpcgrp 17245  SubGrpcsubg 17411  Cntzccntz 17571  LSSumclsm 17872   DProd cdprd 18215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-sbg 17250  df-mulg 17364  df-subg 17414  df-ghm 17481  df-gim 17524  df-cntz 17573  df-oppg 17599  df-lsm 17874  df-cmn 18018  df-dprd 18217
This theorem is referenced by:  dprd2db  18265  dprd2d2  18266
  Copyright terms: Public domain W3C validator