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

Theorem dprd2da 18422
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 2620 . 2 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2620 . 2 (0g𝐺) = (0g𝐺)
3 dprd2d.k . 2 𝐾 = (mrCls‘(SubGrp‘𝐺))
4 dprd2d.5 . . 3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
5 dprdgrp 18385 . . 3 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp)
64, 5syl 17 . 2 (𝜑𝐺 ∈ Grp)
7 resiun2 5406 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = 𝑖𝐼 (𝐴 ↾ {𝑖})
8 iunid 4566 . . . . . 6 𝑖𝐼 {𝑖} = 𝐼
98reseq2i 5382 . . . . 5 (𝐴 𝑖𝐼 {𝑖}) = (𝐴𝐼)
107, 9eqtr3i 2644 . . . 4 𝑖𝐼 (𝐴 ↾ {𝑖}) = (𝐴𝐼)
11 dprd2d.1 . . . . 5 (𝜑 → Rel 𝐴)
12 dprd2d.3 . . . . 5 (𝜑 → dom 𝐴𝐼)
13 relssres 5425 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝐼) → (𝐴𝐼) = 𝐴)
1411, 12, 13syl2anc 692 . . . 4 (𝜑 → (𝐴𝐼) = 𝐴)
1510, 14syl5eq 2666 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) = 𝐴)
16 ovex 6663 . . . . . 6 (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V
17 eqid 2620 . . . . . 6 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
1816, 17dmmpti 6010 . . . . 5 dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼
19 reldmdprd 18377 . . . . . . 7 Rel dom DProd
2019brrelex2i 5149 . . . . . 6 (𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
21 dmexg 7082 . . . . . 6 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
224, 20, 213syl 18 . . . . 5 (𝜑 → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V)
2318, 22syl5eqelr 2704 . . . 4 (𝜑𝐼 ∈ V)
24 ressn 5659 . . . . . 6 (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖}))
25 snex 4899 . . . . . . 7 {𝑖} ∈ V
26 ovex 6663 . . . . . . . . 9 (𝑖𝑆𝑗) ∈ V
27 eqid 2620 . . . . . . . . 9 (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))
2826, 27dmmpti 6010 . . . . . . . 8 dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖})
29 dprd2d.4 . . . . . . . . 9 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
3019brrelex2i 5149 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
31 dmexg 7082 . . . . . . . . 9 ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3229, 30, 313syl 18 . . . . . . . 8 ((𝜑𝑖𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V)
3328, 32syl5eqelr 2704 . . . . . . 7 ((𝜑𝑖𝐼) → (𝐴 “ {𝑖}) ∈ V)
34 xpexg 6945 . . . . . . 7 (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3525, 33, 34sylancr 694 . . . . . 6 ((𝜑𝑖𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V)
3624, 35syl5eqel 2703 . . . . 5 ((𝜑𝑖𝐼) → (𝐴 ↾ {𝑖}) ∈ V)
3736ralrimiva 2963 . . . 4 (𝜑 → ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
38 iunexg 7128 . . . 4 ((𝐼 ∈ V ∧ ∀𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V) → 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
3923, 37, 38syl2anc 692 . . 3 (𝜑 𝑖𝐼 (𝐴 ↾ {𝑖}) ∈ V)
4015, 39eqeltrrd 2700 . 2 (𝜑𝐴 ∈ V)
41 dprd2d.2 . 2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
4212adantr 481 . . . . . . . . 9 ((𝜑𝑥𝐴) → dom 𝐴𝐼)
43 1stdm 7200 . . . . . . . . . 10 ((Rel 𝐴𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
4411, 43sylan 488 . . . . . . . . 9 ((𝜑𝑥𝐴) → (1st𝑥) ∈ dom 𝐴)
4542, 44sseldd 3596 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥) ∈ 𝐼)
4629ralrimiva 2963 . . . . . . . . 9 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
4746adantr 481 . . . . . . . 8 ((𝜑𝑥𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
48 sneq 4178 . . . . . . . . . . . 12 (𝑖 = (1st𝑥) → {𝑖} = {(1st𝑥)})
4948imaeq2d 5454 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑥)}))
50 oveq1 6642 . . . . . . . . . . 11 (𝑖 = (1st𝑥) → (𝑖𝑆𝑗) = ((1st𝑥)𝑆𝑗))
5149, 50mpteq12dv 4724 . . . . . . . . . 10 (𝑖 = (1st𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5251breq2d 4656 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
5352rspcv 3300 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
5445, 47, 53sylc 65 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
55543ad2antr1 1224 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
5655adantr 481 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
57 ovex 6663 . . . . . . 7 ((1st𝑥)𝑆𝑗) ∈ V
58 eqid 2620 . . . . . . 7 (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
5957, 58dmmpti 6010 . . . . . 6 dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)})
6059a1i 11 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
61 1st2nd 7199 . . . . . . . . . . 11 ((Rel 𝐴𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6211, 61sylan 488 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
63 simpr 477 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴)
6462, 63eqeltrrd 2700 . . . . . . . . 9 ((𝜑𝑥𝐴) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
65 df-br 4645 . . . . . . . . 9 ((1st𝑥)𝐴(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐴)
6664, 65sylibr 224 . . . . . . . 8 ((𝜑𝑥𝐴) → (1st𝑥)𝐴(2nd𝑥))
6711adantr 481 . . . . . . . . 9 ((𝜑𝑥𝐴) → Rel 𝐴)
68 elrelimasn 5477 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
6967, 68syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴(2nd𝑥)))
7066, 69mpbird 247 . . . . . . 7 ((𝜑𝑥𝐴) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
71703ad2antr1 1224 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7271adantr 481 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}))
7311adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → Rel 𝐴)
74 simpr2 1066 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦𝐴)
75 1st2nd 7199 . . . . . . . . . . 11 ((Rel 𝐴𝑦𝐴) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7673, 74, 75syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
7776, 74eqeltrrd 2700 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
78 df-br 4645 . . . . . . . . 9 ((1st𝑦)𝐴(2nd𝑦) ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴)
7977, 78sylibr 224 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦)𝐴(2nd𝑦))
80 elrelimasn 5477 . . . . . . . . 9 (Rel 𝐴 → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8173, 80syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) ↔ (1st𝑦)𝐴(2nd𝑦)))
8279, 81mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
8382adantr 481 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}))
84 simpr 477 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (1st𝑥) = (1st𝑦))
8584sneqd 4180 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → {(1st𝑥)} = {(1st𝑦)})
8685imaeq2d 5454 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝐴 “ {(1st𝑥)}) = (𝐴 “ {(1st𝑦)}))
8783, 86eleqtrrd 2702 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
88 simplr3 1103 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → 𝑥𝑦)
89 simpr1 1065 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥𝐴)
9073, 89, 61syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
9190, 76eqeq12d 2635 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩))
92 fvex 6188 . . . . . . . . . 10 (1st𝑥) ∈ V
93 fvex 6188 . . . . . . . . . 10 (2nd𝑥) ∈ V
9492, 93opth 4935 . . . . . . . . 9 (⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦)))
9591, 94syl6bb 276 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑥 = 𝑦 ↔ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥) = (2nd𝑦))))
9695baibd 947 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥 = 𝑦 ↔ (2nd𝑥) = (2nd𝑦)))
9796necon3bid 2835 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑥𝑦 ↔ (2nd𝑥) ≠ (2nd𝑦)))
9888, 97mpbid 222 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (2nd𝑥) ≠ (2nd𝑦))
9956, 60, 72, 87, 98, 1dprdcntz 18388 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))))
100 df-ov 6638 . . . . . 6 ((1st𝑥)𝑆(2nd𝑥)) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩)
101 oveq2 6643 . . . . . . . 8 (𝑗 = (2nd𝑥) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑥)))
102101, 58, 57fvmpt3i 6274 . . . . . . 7 ((2nd𝑥) ∈ (𝐴 “ {(1st𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10371, 102syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
10490fveq2d 6182 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
105100, 103, 1043eqtr4a 2680 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
106105adantr 481 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
10784oveq1d 6650 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((1st𝑥)𝑆𝑗) = ((1st𝑦)𝑆𝑗))
10886, 107mpteq12dv 4724 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
109108fveq1d 6180 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)))
110 df-ov 6638 . . . . . . . 8 ((1st𝑦)𝑆(2nd𝑦)) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩)
111 oveq2 6643 . . . . . . . . . 10 (𝑗 = (2nd𝑦) → ((1st𝑦)𝑆𝑗) = ((1st𝑦)𝑆(2nd𝑦)))
112 eqid 2620 . . . . . . . . . 10 (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))
113 ovex 6663 . . . . . . . . . 10 ((1st𝑦)𝑆𝑗) ∈ V
114111, 112, 113fvmpt3i 6274 . . . . . . . . 9 ((2nd𝑦) ∈ (𝐴 “ {(1st𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11582, 114syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = ((1st𝑦)𝑆(2nd𝑦)))
11676fveq2d 6182 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
117110, 115, 1163eqtr4a 2680 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
118117adantr 481 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
119109, 118eqtrd 2654 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦)) = (𝑆𝑦))
120119fveq2d 6182 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑦))) = ((Cntz‘𝐺)‘(𝑆𝑦)))
12199, 106, 1203sstr3d 3639 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) = (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
12211, 41, 12, 29, 4, 3dprd2dlem2 18420 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12351oveq2d 6651 . . . . . . . . 9 (𝑖 = (1st𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
124123, 17, 16fvmpt3i 6274 . . . . . . . 8 ((1st𝑥) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
12545, 124syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
126122, 125sseqtr4d 3634 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1271263ad2antr1 1224 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
128127adantr 481 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
1294ad2antrr 761 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
13018a1i 11 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
131453ad2antr1 1224 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑥) ∈ 𝐼)
132131adantr 481 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ∈ 𝐼)
13312adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom 𝐴𝐼)
134 1stdm 7200 . . . . . . . . 9 ((Rel 𝐴𝑦𝐴) → (1st𝑦) ∈ dom 𝐴)
13573, 74, 134syl2anc 692 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ dom 𝐴)
136133, 135sseldd 3596 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (1st𝑦) ∈ 𝐼)
137136adantr 481 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑦) ∈ 𝐼)
138 simpr 477 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (1st𝑥) ≠ (1st𝑦))
139129, 130, 132, 137, 138, 1dprdcntz 18388 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))))
140 sneq 4178 . . . . . . . . . . . . 13 (𝑖 = (1st𝑦) → {𝑖} = {(1st𝑦)})
141140imaeq2d 5454 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑦)}))
142 oveq1 6642 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝑖𝑆𝑗) = ((1st𝑦)𝑆𝑗))
143141, 142mpteq12dv 4724 . . . . . . . . . . 11 (𝑖 = (1st𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
144143oveq2d 6651 . . . . . . . . . 10 (𝑖 = (1st𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
145144, 17, 16fvmpt3i 6274 . . . . . . . . 9 ((1st𝑦) ∈ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
146136, 145syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
147146fveq2d 6182 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))))
148 eqid 2620 . . . . . . . . 9 (Base‘𝐺) = (Base‘𝐺)
149148dprdssv 18396 . . . . . . . 8 (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))) ⊆ (Base‘𝐺)
15046adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
151143breq2d 4656 . . . . . . . . . . . 12 (𝑖 = (1st𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
152151rspcv 3300 . . . . . . . . . . 11 ((1st𝑦) ∈ 𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
153136, 150, 152sylc 65 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)))
154113, 112dmmpti 6010 . . . . . . . . . . 11 dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)})
155154a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗)) = (𝐴 “ {(1st𝑦)}))
156153, 155, 82dprdub 18405 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))‘(2nd𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
157117, 156eqsstr3d 3632 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑦)}) ↦ ((1st𝑦)𝑆𝑗))))
158148, 1cntz2ss 17746 . . . . . . . 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 3631 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
161160adantr 481 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((Cntz‘𝐺)‘((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
162139, 161sstrd 3605 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
163128, 162sstrd 3605 . . 3 (((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) ∧ (1st𝑥) ≠ (1st𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
164121, 163pm2.61dane 2878 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
1656adantr 481 . . . . . 6 ((𝜑𝑥𝐴) → 𝐺 ∈ Grp)
166148subgacs 17610 . . . . . 6 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
167 acsmre 16294 . . . . . 6 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
168165, 166, 1673syl 18 . . . . 5 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
16914adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = 𝐴)
170 undif2 4035 . . . . . . . . . . . . . . . . . 18 ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})) = ({(1st𝑥)} ∪ 𝐼)
17145snssd 4331 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐴) → {(1st𝑥)} ⊆ 𝐼)
172 ssequn1 3775 . . . . . . . . . . . . . . . . . . 19 ({(1st𝑥)} ⊆ 𝐼 ↔ ({(1st𝑥)} ∪ 𝐼) = 𝐼)
173171, 172sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∪ 𝐼) = 𝐼)
174170, 173syl5req 2667 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐼 = ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)})))
175174reseq2d 5385 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝐴𝐼) = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
176169, 175eqtr3d 2656 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐴 = (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))))
177 resundi 5398 . . . . . . . . . . . . . . 15 (𝐴 ↾ ({(1st𝑥)} ∪ (𝐼 ∖ {(1st𝑥)}))) = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
178176, 177syl6eq 2670 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = ((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
179178difeq1d 3719 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}))
180 difundir 3872 . . . . . . . . . . . . 13 (((𝐴 ↾ {(1st𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
181179, 180syl6eq 2670 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})))
182 neirr 2800 . . . . . . . . . . . . . . . . 17 ¬ (1st𝑥) ≠ (1st𝑥)
18362eleq1d 2684 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
184 df-br 4645 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
18593brres 5391 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) ↔ ((1st𝑥)𝐴(2nd𝑥) ∧ (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)})))
186185simprbi 480 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}))
187 eldifsni 4311 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ (𝐼 ∖ {(1st𝑥)}) → (1st𝑥) ≠ (1st𝑥))
188186, 187syl 17 . . . . . . . . . . . . . . . . . . 19 ((1st𝑥)(𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))(2nd𝑥) → (1st𝑥) ≠ (1st𝑥))
189184, 188sylbir 225 . . . . . . . . . . . . . . . . . 18 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥))
190183, 189syl6bi 243 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) → (1st𝑥) ≠ (1st𝑥)))
191182, 190mtoi 190 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
192 disjsn 4237 . . . . . . . . . . . . . . . 16 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
193191, 192sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅)
194 disj3 4012 . . . . . . . . . . . . . . 15 (((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
195193, 194sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}))
196195eqcomd 2626 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))
197196uneq2d 3759 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
198181, 197eqtrd 2654 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
199198imaeq2d 5454 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
200 imaundi 5533 . . . . . . . . . 10 (𝑆 “ (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
201199, 200syl6eq 2670 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
202201unieqd 4437 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
203 uniun 4447 . . . . . . . 8 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))
204202, 203syl6eq 2670 . . . . . . 7 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
205 imassrn 5465 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆
206 frn 6040 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺))
20741, 206syl 17 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺))
208207adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺))
209 mresspw 16233 . . . . . . . . . . . . 13 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
210168, 209syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
211208, 210sstrd 3605 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺))
212205, 211syl5ss 3606 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
213 sspwuni 4602 . . . . . . . . . 10 ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
214212, 213sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺))
215168, 3, 214mrcssidd 16266 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
216 imassrn 5465 . . . . . . . . . . 11 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ ran 𝑆
217216, 211syl5ss 3606 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺))
218 sspwuni 4602 . . . . . . . . . 10 ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
219217, 218sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺))
220168, 3, 219mrcssidd 16266 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
221 unss12 3777 . . . . . . . 8 (( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
222215, 220, 221syl2anc 692 . . . . . . 7 ((𝜑𝑥𝐴) → ( (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
223204, 222eqsstrd 3631 . . . . . 6 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
2243mrccl 16252 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
225168, 214, 224syl2anc 692 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
2263mrccl 16252 . . . . . . . 8 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
227168, 219, 226syl2anc 692 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺))
228 eqid 2620 . . . . . . . 8 (LSSum‘𝐺) = (LSSum‘𝐺)
229228lsmunss 18054 . . . . . . 7 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺)) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
230225, 227, 229syl2anc 692 . . . . . 6 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∪ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
231223, 230sstrd 3605 . . . . 5 ((𝜑𝑥𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
232 difss 3729 . . . . . . . . . . . . 13 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st𝑥)})
233 ressn 5659 . . . . . . . . . . . . 13 (𝐴 ↾ {(1st𝑥)}) = ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
234232, 233sseqtri 3629 . . . . . . . . . . . 12 ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))
235 imass2 5489 . . . . . . . . . . . 12 (((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))))
236234, 235ax-mp 5 . . . . . . . . . . 11 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
237 ovex 6663 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝑆𝑖) ∈ V
238 oveq2 6643 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆𝑖))
23958, 238elrnmpt1s 5362 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝐴 “ {(1st𝑥)}) ∧ ((1st𝑥)𝑆𝑖) ∈ V) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
240237, 239mpan2 706 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝐴 “ {(1st𝑥)}) → ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
241240rgen 2919 . . . . . . . . . . . . . 14 𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
242241a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
243 oveq1 6642 . . . . . . . . . . . . . . . 16 (𝑦 = (1st𝑥) → (𝑦𝑆𝑖) = ((1st𝑥)𝑆𝑖))
244243eleq1d 2684 . . . . . . . . . . . . . . 15 (𝑦 = (1st𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
245244ralbidv 2983 . . . . . . . . . . . . . 14 (𝑦 = (1st𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
24692, 245ralsn 4213 . . . . . . . . . . . . 13 (∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st𝑥)})((1st𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
247242, 246sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
24841adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺))
249 ffun 6035 . . . . . . . . . . . . . 14 (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆)
250248, 249syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun 𝑆)
251 resss 5410 . . . . . . . . . . . . . . 15 (𝐴 ↾ {(1st𝑥)}) ⊆ 𝐴
252233, 251eqsstr3i 3628 . . . . . . . . . . . . . 14 ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ 𝐴
253 fdm 6038 . . . . . . . . . . . . . . 15 (𝑆:𝐴⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐴)
254248, 253syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → dom 𝑆 = 𝐴)
255252, 254syl5sseqr 3646 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆)
256 funimassov 6796 . . . . . . . . . . . . 13 ((Fun 𝑆 ∧ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) ⊆ dom 𝑆) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
257250, 255, 256syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st𝑥)}∀𝑖 ∈ (𝐴 “ {(1st𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
258247, 257mpbird 247 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑆 “ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
259236, 258syl5ss 3606 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
260259unissd 4453 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))
261 df-ov 6638 . . . . . . . . . . . . . 14 ((1st𝑥)𝑆𝑗) = (𝑆‘⟨(1st𝑥), 𝑗⟩)
26241ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺))
263 elrelimasn 5477 . . . . . . . . . . . . . . . . . 18 (Rel 𝐴 → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
26467, 263syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↔ (1st𝑥)𝐴𝑗))
265264biimpa 501 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (1st𝑥)𝐴𝑗)
266 df-br 4645 . . . . . . . . . . . . . . . 16 ((1st𝑥)𝐴𝑗 ↔ ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
267265, 266sylib 208 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ⟨(1st𝑥), 𝑗⟩ ∈ 𝐴)
268262, 267ffvelrnd 6346 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → (𝑆‘⟨(1st𝑥), 𝑗⟩) ∈ (SubGrp‘𝐺))
269261, 268syl5eqel 2703 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st𝑥)})) → ((1st𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺))
270269, 58fmptd 6371 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺))
271 frn 6040 . . . . . . . . . . . 12 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)):(𝐴 “ {(1st𝑥)})⟶(SubGrp‘𝐺) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
272270, 271syl 17 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺))
273272, 210sstrd 3605 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺))
274 sspwuni 4602 . . . . . . . . . 10 (ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
275273, 274sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ⊆ (Base‘𝐺))
276168, 3, 260, 275mrcssd 16265 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2773dprdspan 18407 . . . . . . . . 9 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
27854, 277syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) = (𝐾 ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
279276, 278sseqtr4d 3634 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
28016, 17fnmpti 6009 . . . . . . . . . . . . 13 (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼
281 fnressn 6410 . . . . . . . . . . . . 13 (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st𝑥) ∈ 𝐼) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
282280, 45, 281sylancr 694 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩})
283125opeq2d 4400 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩ = ⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩)
284283sneqd 4180 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → {⟨(1st𝑥), ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥))⟩} = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
285282, 284eqtrd 2654 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)}) = {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩})
286285oveq2d 6651 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}))
287 dprdsubg 18404 . . . . . . . . . . . . 13 (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
28854, 287syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺))
289 dprdsn 18416 . . . . . . . . . . . 12 (((1st𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
29045, 288, 289syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺dom DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩} ∧ (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
291290simprd 479 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd {⟨(1st𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))⟩}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
292286, 291eqtrd 2654 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
2934adantr 481 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
29418a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → dom (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼)
295 difss 3729 . . . . . . . . . . 11 (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼
296295a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼)
297 disjdif 4031 . . . . . . . . . . 11 ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅
298297a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ({(1st𝑥)} ∩ (𝐼 ∖ {(1st𝑥)})) = ∅)
299293, 294, 171, 296, 298, 1dprdcntz2 18418 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
300292, 299eqsstr3d 3632 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
30129adantlr 750 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
30267, 248, 42, 301, 293, 3, 296dprd2dlem1 18421 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))
303 resmpt 5437 . . . . . . . . . . . 12 ((𝐼 ∖ {(1st𝑥)}) ⊆ 𝐼 → ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
304295, 303ax-mp 5 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))
305304oveq2i 6646 . . . . . . . . . 10 (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
306302, 305syl6eqr 2672 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
307306fveq2d 6182 . . . . . . . 8 ((𝜑𝑥𝐴) → ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))))
308300, 307sseqtr4d 3634 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
309279, 308sstrd 3605 . . . . . 6 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
310228, 1lsmsubg 18050 . . . . . 6 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
311225, 227, 309, 310syl3anc 1324 . . . . 5 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺))
3123mrcsscl 16261 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∧ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ∈ (SubGrp‘𝐺)) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
313168, 231, 311, 312syl3anc 1324 . . . 4 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
314 sslin 3831 . . . 4 ((𝐾 (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
315313, 314syl 17 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))))
31641ffvelrnda 6345 . . . 4 ((𝜑𝑥𝐴) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
317228lsmlub 18059 . . . . . . . . . 10 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
318225, 316, 288, 317syl3anc 1324 . . . . . . . . 9 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))) ∧ (𝑆𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))) ↔ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)))))
319279, 122, 318mpbi2and 955 . . . . . . . 8 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))))
320319, 125sseqtr4d 3634 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)))
321293, 294, 296dprdres 18408 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) ∧ (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) ⊆ (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))))
322321simpld 475 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
3233dprdspan 18407 . . . . . . . . . . 11 (𝐺dom DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
324322, 323syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))))
325 df-ima 5117 . . . . . . . . . . . 12 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
326325unieqi 4436 . . . . . . . . . . 11 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})) = ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))
327326fveq2i 6181 . . . . . . . . . 10 (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ran ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)})))
328324, 327syl6eqr 2672 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐺 DProd ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st𝑥)}))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
329306, 328eqtrd 2654 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
330 eqimss 3649 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) = (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
331329, 330syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)}))))
332 ss2in 3832 . . . . . . 7 ((((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ⊆ ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∧ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ⊆ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
333320, 331, 332syl2anc 692 . . . . . 6 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))))
334293, 294, 45, 2, 3dprddisj 18389 . . . . . 6 ((𝜑𝑥𝐴) → (((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st𝑥)) ∩ (𝐾 ((𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st𝑥)})))) = {(0g𝐺)})
335333, 334sseqtrd 3633 . . . . 5 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) ⊆ {(0g𝐺)})
336228lsmub2 18053 . . . . . . . . 9 (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆𝑥) ∈ (SubGrp‘𝐺)) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
337225, 316, 336syl2anc 692 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3382subg0cl 17583 . . . . . . . . 9 ((𝑆𝑥) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑆𝑥))
339316, 338syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝑆𝑥))
340337, 339sseldd 3596 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)))
3412subg0cl 17583 . . . . . . . 8 ((𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
342227, 341syl 17 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))
343340, 342elind 3790 . . . . . 6 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
344343snssd 4331 . . . . 5 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))))
345335, 344eqssd 3612 . . . 4 ((𝜑𝑥𝐴) → (((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆𝑥)) ∩ (𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)}))))) = {(0g𝐺)})
346 incom 3797 . . . . 5 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
34770, 102syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = ((1st𝑥)𝑆(2nd𝑥)))
34862fveq2d 6182 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆𝑥) = (𝑆‘⟨(1st𝑥), (2nd𝑥)⟩))
349100, 347, 3483eqtr4a 2680 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥))
350 eqimss2 3650 . . . . . . . . 9 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) = (𝑆𝑥) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
351349, 350syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)))
352 eldifsn 4308 . . . . . . . . . . . . 13 (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥))
35311ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → Rel 𝐴)
354 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st𝑥)}))
355251, 354sseldi 3593 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝐴)
356353, 355, 75syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
357356fveq2d 6182 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = (𝑆‘⟨(1st𝑦), (2nd𝑦)⟩))
358357, 110syl6eqr 2672 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑦)𝑆(2nd𝑦)))
359356, 354eqeltrrd 2700 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}))
360 fvex 6188 . . . . . . . . . . . . . . . . . . . . . 22 (2nd𝑦) ∈ V
361360opelres 5390 . . . . . . . . . . . . . . . . . . . . 21 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) ↔ (⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝐴 ∧ (1st𝑦) ∈ {(1st𝑥)}))
362361simprbi 480 . . . . . . . . . . . . . . . . . . . 20 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝐴 ↾ {(1st𝑥)}) → (1st𝑦) ∈ {(1st𝑥)})
363359, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) ∈ {(1st𝑥)})
364 elsni 4185 . . . . . . . . . . . . . . . . . . 19 ((1st𝑦) ∈ {(1st𝑥)} → (1st𝑦) = (1st𝑥))
365363, 364syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (1st𝑦) = (1st𝑥))
366365oveq1d 6650 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → ((1st𝑦)𝑆(2nd𝑦)) = ((1st𝑥)𝑆(2nd𝑦)))
367358, 366eqtrd 2654 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) = ((1st𝑥)𝑆(2nd𝑦)))
368354, 233syl6eleq 2709 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})))
369 xp2nd 7184 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ({(1st𝑥)} × (𝐴 “ {(1st𝑥)})) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
370368, 369syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}))
371 simprr 795 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑦𝑥)
37262adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
373356, 372eqeq12d 2635 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩))
374 fvex 6188 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st𝑦) ∈ V
375374, 360opth 4935 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ ((1st𝑦) = (1st𝑥) ∧ (2nd𝑦) = (2nd𝑥)))
376375baib 943 . . . . . . . . . . . . . . . . . . . . . 22 ((1st𝑦) = (1st𝑥) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
377365, 376syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (⟨(1st𝑦), (2nd𝑦)⟩ = ⟨(1st𝑥), (2nd𝑥)⟩ ↔ (2nd𝑦) = (2nd𝑥)))
378373, 377bitrd 268 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦 = 𝑥 ↔ (2nd𝑦) = (2nd𝑥)))
379378necon3bid 2835 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑦𝑥 ↔ (2nd𝑦) ≠ (2nd𝑥)))
380371, 379mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ≠ (2nd𝑥))
381 eldifsn 4308 . . . . . . . . . . . . . . . . . 18 ((2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ↔ ((2nd𝑦) ∈ (𝐴 “ {(1st𝑥)}) ∧ (2nd𝑦) ≠ (2nd𝑥)))
382370, 380, 381sylanbrc 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (2nd𝑦) ∈ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
383 ovex 6663 . . . . . . . . . . . . . . . . 17 ((1st𝑥)𝑆(2nd𝑦)) ∈ V
384 difss 3729 . . . . . . . . . . . . . . . . . . 19 ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}) ⊆ (𝐴 “ {(1st𝑥)})
385 resmpt 5437 . . . . . . . . . . . . . . . . . . 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 6643 . . . . . . . . . . . . . . . . . 18 (𝑗 = (2nd𝑦) → ((1st𝑥)𝑆𝑗) = ((1st𝑥)𝑆(2nd𝑦)))
388386, 387elrnmpt1s 5362 . . . . . . . . . . . . . . . . 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 2699 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
391 df-ima 5117 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))
392390, 391syl6eleqr 2710 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥)) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
393392ex 450 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st𝑥)}) ∧ 𝑦𝑥) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
394352, 393syl5bi 232 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) → (𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
395394ralrimiv 2962 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
396234, 255syl5ss 3606 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆)
397 funimass4 6234 . . . . . . . . . . . 12 ((Fun 𝑆 ∧ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
398250, 396, 397syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ↔ ∀𝑦 ∈ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})(𝑆𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
399395, 398mpbird 247 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
400399unissd 4453 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))
401 imassrn 5465 . . . . . . . . . . 11 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))
402401, 273syl5ss 3606 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺))
403 sspwuni 4602 . . . . . . . . . 10 (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ 𝒫 (Base‘𝐺) ↔ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
404402, 403sylib 208 . . . . . . . . 9 ((𝜑𝑥𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})) ⊆ (Base‘𝐺))
405168, 3, 400, 404mrcssd 16265 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)}))))
406 ss2in 3832 . . . . . . . 8 (((𝑆𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∧ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ⊆ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
407351, 405, 406syl2anc 692 . . . . . . 7 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))))
40859a1i 11 . . . . . . . 8 ((𝜑𝑥𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) = (𝐴 “ {(1st𝑥)}))
40954, 408, 70, 2, 3dprddisj 18389 . . . . . . 7 ((𝜑𝑥𝐴) → (((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗))‘(2nd𝑥)) ∩ (𝐾 ((𝑗 ∈ (𝐴 “ {(1st𝑥)}) ↦ ((1st𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st𝑥)}) ∖ {(2nd𝑥)})))) = {(0g𝐺)})
410407, 409sseqtrd 3633 . . . . . 6 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) ⊆ {(0g𝐺)})
4112subg0cl 17583 . . . . . . . . 9 ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
412225, 411syl 17 . . . . . . . 8 ((𝜑𝑥𝐴) → (0g𝐺) ∈ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))))
413339, 412elind 3790 . . . . . . 7 ((𝜑𝑥𝐴) → (0g𝐺) ∈ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
414413snssd 4331 . . . . . 6 ((𝜑𝑥𝐴) → {(0g𝐺)} ⊆ ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))))
415410, 414eqssd 3612 . . . . 5 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))) = {(0g𝐺)})
416346, 415syl5eq 2666 . . . 4 ((𝜑𝑥𝐴) → ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥}))) ∩ (𝑆𝑥)) = {(0g𝐺)})
417228, 225, 316, 227, 2, 345, 416lsmdisj2 18076 . . 3 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ ((𝐾 (𝑆 “ ((𝐴 ↾ {(1st𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾 (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st𝑥)})))))) = {(0g𝐺)})
418315, 417sseqtrd 3633 . 2 ((𝜑𝑥𝐴) → ((𝑆𝑥) ∩ (𝐾 (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g𝐺)})
4191, 2, 3, 6, 40, 41, 164, 418dmdprdd 18379 1 (𝜑𝐺dom DProd 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  Vcvv 3195  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168  cop 4174   cuni 4427   ciun 4511   class class class wbr 4644  cmpt 4720   × cxp 5102  dom cdm 5104  ran crn 5105  cres 5106  cima 5107  Rel wrel 5109  Fun wfun 5870   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  1st c1st 7151  2nd c2nd 7152  Basecbs 15838  0gc0g 16081  Moorecmre 16223  mrClscmrc 16224  ACScacs 16226  Grpcgrp 17403  SubGrpcsubg 17569  Cntzccntz 17729  LSSumclsm 18030   DProd cdprd 18373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-tpos 7337  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-2 11064  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-fzo 12450  df-seq 12785  df-hash 13101  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-0g 16083  df-gsum 16084  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-mhm 17316  df-submnd 17317  df-grp 17406  df-minusg 17407  df-sbg 17408  df-mulg 17522  df-subg 17572  df-ghm 17639  df-gim 17682  df-cntz 17731  df-oppg 17757  df-lsm 18032  df-cmn 18176  df-dprd 18375
This theorem is referenced by:  dprd2db  18423  dprd2d2  18424
  Copyright terms: Public domain W3C validator