Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | eqid 2737 |
. 2
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | dprd2d.k |
. 2
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
4 | | dprd2d.5 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
5 | | dprdgrp 19392 |
. . 3
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | resiun2 5872 |
. . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪
𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) |
8 | | iunid 4969 |
. . . . . 6
⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼 |
9 | 8 | reseq2i 5848 |
. . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼) |
10 | 7, 9 | eqtr3i 2767 |
. . . 4
⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼) |
11 | | dprd2d.1 |
. . . . 5
⊢ (𝜑 → Rel 𝐴) |
12 | | dprd2d.3 |
. . . . 5
⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) |
13 | | relssres 5892 |
. . . . 5
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴) |
14 | 11, 12, 13 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴) |
15 | 10, 14 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴) |
16 | | ovex 7246 |
. . . . . 6
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V |
17 | | eqid 2737 |
. . . . . 6
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
18 | 16, 17 | dmmpti 6522 |
. . . . 5
⊢ dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼 |
19 | | reldmdprd 19384 |
. . . . . . 7
⊢ Rel dom
DProd |
20 | 19 | brrelex2i 5606 |
. . . . . 6
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
21 | | dmexg 7681 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
22 | 4, 20, 21 | 3syl 18 |
. . . . 5
⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
23 | 18, 22 | eqeltrrid 2843 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
24 | | ressn 6148 |
. . . . . 6
⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖})) |
25 | | snex 5324 |
. . . . . . 7
⊢ {𝑖} ∈ V |
26 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑖𝑆𝑗) ∈ V |
27 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) |
28 | 26, 27 | dmmpti 6522 |
. . . . . . . 8
⊢ dom
(𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖}) |
29 | | dprd2d.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
30 | 19 | brrelex2i 5606 |
. . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
31 | | dmexg 7681 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
33 | 28, 32 | eqeltrrid 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V) |
34 | | xpexg 7535 |
. . . . . . 7
⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) |
35 | 25, 33, 34 | sylancr 590 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) |
36 | 24, 35 | eqeltrid 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V) |
37 | 36 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
38 | | iunexg 7736 |
. . . 4
⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
39 | 23, 37, 38 | syl2anc 587 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
40 | 15, 39 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → 𝐴 ∈ V) |
41 | | dprd2d.2 |
. 2
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
42 | | sneq 4551 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → {𝑖} = {(1st ‘𝑥)}) |
43 | 42 | imaeq2d 5929 |
. . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑥)})) |
44 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑥) → (𝑖𝑆𝑗) = ((1st ‘𝑥)𝑆𝑗)) |
45 | 43, 44 | mpteq12dv 5140 |
. . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
46 | 45 | breq2d 5065 |
. . . . . . . 8
⊢ (𝑖 = (1st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
47 | 29 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
48 | 47 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
49 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼) |
50 | | 1stdm 7811 |
. . . . . . . . . 10
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
51 | 11, 50 | sylan 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
52 | 49, 51 | sseldd 3902 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ 𝐼) |
53 | 46, 48, 52 | rspcdva 3539 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
54 | 53 | 3ad2antr1 1190 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
55 | 54 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
56 | | ovex 7246 |
. . . . . . 7
⊢
((1st ‘𝑥)𝑆𝑗) ∈ V |
57 | | eqid 2737 |
. . . . . . 7
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) |
58 | 56, 57 | dmmpti 6522 |
. . . . . 6
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)}) |
59 | 58 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) |
60 | | 1st2nd 7810 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
61 | 11, 60 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
62 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
63 | 61, 62 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) |
64 | | df-br 5054 |
. . . . . . . . 9
⊢
((1st ‘𝑥)𝐴(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) |
65 | 63, 64 | sylibr 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥)𝐴(2nd ‘𝑥)) |
66 | 11 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴) |
67 | | elrelimasn 5953 |
. . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)}) ↔
(1st ‘𝑥)𝐴(2nd ‘𝑥))) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴(2nd ‘𝑥))) |
69 | 65, 68 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) |
70 | 69 | 3ad2antr1 1190 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) |
71 | 70 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)})) |
72 | 11 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴) |
73 | | simpr2 1197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴) |
74 | | 1st2nd 7810 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
75 | 72, 73, 74 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
76 | 75, 73 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) |
77 | | df-br 5054 |
. . . . . . . . 9
⊢
((1st ‘𝑦)𝐴(2nd ‘𝑦) ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) |
78 | 76, 77 | sylibr 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦)𝐴(2nd ‘𝑦)) |
79 | | elrelimasn 5953 |
. . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)}) ↔
(1st ‘𝑦)𝐴(2nd ‘𝑦))) |
80 | 72, 79 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) ↔ (1st
‘𝑦)𝐴(2nd ‘𝑦))) |
81 | 78, 80 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)})) |
82 | 81 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)})) |
83 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (1st
‘𝑥) = (1st
‘𝑦)) |
84 | 83 | sneqd 4553 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → {(1st
‘𝑥)} =
{(1st ‘𝑦)}) |
85 | 84 | imaeq2d 5929 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝐴 “ {(1st ‘𝑥)}) = (𝐴 “ {(1st ‘𝑦)})) |
86 | 82, 85 | eleqtrrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑥)})) |
87 | | simplr3 1219 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝑥 ≠ 𝑦) |
88 | | simpr1 1196 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴) |
89 | 72, 88, 60 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
90 | 89, 75 | eqeq12d 2753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉)) |
91 | | fvex 6730 |
. . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V |
92 | | fvex 6730 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
93 | 91, 92 | opth 5360 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) |
94 | 90, 93 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) = (2nd
‘𝑦)))) |
95 | 94 | baibd 543 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
96 | 95 | necon3bid 2985 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2nd ‘𝑥) ≠ (2nd
‘𝑦))) |
97 | 87, 96 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ≠
(2nd ‘𝑦)) |
98 | 55, 59, 71, 86, 97, 1 | dprdcntz 19395 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)))) |
99 | | df-ov 7216 |
. . . . . 6
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥)) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
100 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑗 = (2nd ‘𝑥) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑥))) |
101 | 100, 57, 56 | fvmpt3i 6823 |
. . . . . . 7
⊢
((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
102 | 70, 101 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
103 | 89 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
104 | 99, 102, 103 | 3eqtr4a 2804 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
105 | 104 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
106 | 83 | oveq1d 7228 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) |
107 | 85, 106 | mpteq12dv 5140 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
108 | 107 | fveq1d 6719 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦))) |
109 | | df-ov 7216 |
. . . . . . . 8
⊢
((1st ‘𝑦)𝑆(2nd ‘𝑦)) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
110 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑦)𝑆𝑗) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) |
111 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) |
112 | | ovex 7246 |
. . . . . . . . . 10
⊢
((1st ‘𝑦)𝑆𝑗) ∈ V |
113 | 110, 111,
112 | fvmpt3i 6823 |
. . . . . . . . 9
⊢
((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) |
114 | 81, 113 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) |
115 | 75 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
116 | 109, 114,
115 | 3eqtr4a 2804 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
117 | 116 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
118 | 108, 117 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
119 | 118 | fveq2d 6721 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
120 | 98, 105, 119 | 3sstr3d 3947 |
. . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
121 | 11, 41, 12, 29, 4, 3 | dprd2dlem2 19427 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
122 | 45 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
123 | 122, 17, 16 | fvmpt3i 6823 |
. . . . . . . 8
⊢
((1st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
124 | 52, 123 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
125 | 121, 124 | sseqtrrd 3942 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
126 | 125 | 3ad2antr1 1190 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
127 | 126 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
128 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
129 | 18 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
130 | 52 | 3ad2antr1 1190 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑥) ∈ 𝐼) |
131 | 130 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
∈ 𝐼) |
132 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼) |
133 | | 1stdm 7811 |
. . . . . . . . 9
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ dom 𝐴) |
134 | 72, 73, 133 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ dom 𝐴) |
135 | 132, 134 | sseldd 3902 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ 𝐼) |
136 | 135 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑦)
∈ 𝐼) |
137 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
≠ (1st ‘𝑦)) |
138 | 128, 129,
131, 136, 137, 1 | dprdcntz 19395 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)))) |
139 | | sneq 4551 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑦) → {𝑖} = {(1st ‘𝑦)}) |
140 | 139 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑦)})) |
141 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝑖𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) |
142 | 140, 141 | mpteq12dv 5140 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
143 | 142 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
144 | 143, 17, 16 | fvmpt3i 6823 |
. . . . . . . . 9
⊢
((1st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
145 | 135, 144 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
146 | 145 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))))) |
147 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
148 | 147 | dprdssv 19403 |
. . . . . . . 8
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) |
149 | 142 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
150 | 47 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
151 | 149, 150,
135 | rspcdva 3539 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
152 | 112, 111 | dmmpti 6522 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑦)}) ↦
((1st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)}) |
153 | 152 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)})) |
154 | 151, 153,
81 | dprdub 19412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
155 | 116, 154 | eqsstrrd 3940 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
156 | 147, 1 | cntz2ss 18727 |
. . . . . . . 8
⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
157 | 148, 155,
156 | sylancr 590 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
158 | 146, 157 | eqsstrd 3939 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
159 | 158 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
160 | 138, 159 | sstrd 3911 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
161 | 127, 160 | sstrd 3911 |
. . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
162 | 120, 161 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
163 | 6 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp) |
164 | 147 | subgacs 18577 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
165 | | acsmre 17155 |
. . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
166 | 163, 164,
165 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
167 | 14 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴) |
168 | | undif2 4391 |
. . . . . . . . . . . . . . . . . 18
⊢
({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})) = ({(1st
‘𝑥)} ∪ 𝐼) |
169 | 52 | snssd 4722 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1st ‘𝑥)} ⊆ 𝐼) |
170 | | ssequn1 4094 |
. . . . . . . . . . . . . . . . . . 19
⊢
({(1st ‘𝑥)} ⊆ 𝐼 ↔ ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) |
171 | 169, 170 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) |
172 | 168, 171 | eqtr2id 2791 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)}))) |
173 | 172 | reseq2d 5851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) |
174 | 167, 173 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) |
175 | | resundi 5865 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ ({(1st
‘𝑥)} ∪ (𝐼 ∖ {(1st
‘𝑥)}))) = ((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
176 | 174, 175 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
177 | 176 | difeq1d 4036 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥})) |
178 | | difundir 4195 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
179 | 177, 178 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}))) |
180 | | neirr 2949 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(1st ‘𝑥)
≠ (1st ‘𝑥) |
181 | 61 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ↔
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
182 | | df-br 5054 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∈
(𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) |
183 | 92 | brresi 5860 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ ((1st
‘𝑥) ∈ (𝐼 ∖ {(1st
‘𝑥)}) ∧
(1st ‘𝑥)𝐴(2nd ‘𝑥))) |
184 | 183 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ∈ (𝐼 ∖ {(1st
‘𝑥)})) |
185 | | eldifsni 4703 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥) ∈ (𝐼 ∖ {(1st ‘𝑥)}) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
187 | 182, 186 | sylbir 238 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
188 | 181, 187 | syl6bi 256 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥))) |
189 | 180, 188 | mtoi 202 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
190 | | disjsn 4627 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
191 | 189, 190 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅) |
192 | | disj3 4368 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
193 | 191, 192 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
194 | 193 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
195 | 194 | uneq2d 4077 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
196 | 179, 195 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
197 | 196 | imaeq2d 5929 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
198 | | imaundi 6013 |
. . . . . . . . . 10
⊢ (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
199 | 197, 198 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
200 | 199 | unieqd 4833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
201 | | uniun 4844 |
. . . . . . . 8
⊢ ∪ ((𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
202 | 200, 201 | eqtrdi 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
203 | | imassrn 5940 |
. . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆 |
204 | 41 | frnd 6553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
205 | 204 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
206 | | mresspw 17095 |
. . . . . . . . . . . . 13
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
207 | 166, 206 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
208 | 205, 207 | sstrd 3911 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
209 | 203, 208 | sstrid 3912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
210 | | sspwuni 5008 |
. . . . . . . . . 10
⊢ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) |
211 | 209, 210 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) |
212 | 166, 3, 211 | mrcssidd 17128 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
213 | | imassrn 5940 |
. . . . . . . . . . 11
⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ ran 𝑆 |
214 | 213, 208 | sstrid 3912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺)) |
215 | | sspwuni 5008 |
. . . . . . . . . 10
⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺) ↔ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) ⊆
(Base‘𝐺)) |
216 | 214, 215 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) |
217 | 166, 3, 216 | mrcssidd 17128 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
218 | | unss12 4096 |
. . . . . . . 8
⊢ ((∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪
(𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
219 | 212, 217,
218 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪
(𝑆 “ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ⊆
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
220 | 202, 219 | eqsstrd 3939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
221 | 3 | mrccl 17114 |
. . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
222 | 166, 211,
221 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
223 | 3 | mrccl 17114 |
. . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) |
224 | 166, 216,
223 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) |
225 | | eqid 2737 |
. . . . . . . 8
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
226 | 225 | lsmunss 19048 |
. . . . . . 7
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) →
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
227 | 222, 224,
226 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
228 | 220, 227 | sstrd 3911 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
229 | | difss 4046 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st ‘𝑥)}) |
230 | | ressn 6148 |
. . . . . . . . . . . . 13
⊢ (𝐴 ↾ {(1st
‘𝑥)}) =
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) |
231 | 229, 230 | sseqtri 3937 |
. . . . . . . . . . . 12
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) |
232 | | imass2 5970 |
. . . . . . . . . . . 12
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})))) |
233 | 231, 232 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) |
234 | | ovex 7246 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝑆𝑖) ∈ V |
235 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → ((1st ‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆𝑖)) |
236 | 57, 235 | elrnmpt1s 5826 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) ∧ ((1st
‘𝑥)𝑆𝑖) ∈ V) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
237 | 234, 236 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
238 | 237 | rgen 3071 |
. . . . . . . . . . . . . 14
⊢
∀𝑖 ∈
(𝐴 “ {(1st
‘𝑥)})((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) |
239 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
240 | | oveq1 7220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (1st ‘𝑥) → (𝑦𝑆𝑖) = ((1st ‘𝑥)𝑆𝑖)) |
241 | 240 | eleq1d 2822 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (1st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
242 | 241 | ralbidv 3118 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
243 | 91, 242 | ralsn 4597 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
{(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
244 | 239, 243 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
245 | 41 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
246 | 245 | ffund 6549 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆) |
247 | | resss 5876 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ {(1st
‘𝑥)}) ⊆ 𝐴 |
248 | 230, 247 | eqsstrri 3936 |
. . . . . . . . . . . . . 14
⊢
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ 𝐴 |
249 | 245 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴) |
250 | 248, 249 | sseqtrrid 3954 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ dom 𝑆) |
251 | | funimassov 7385 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑆 ∧ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) ⊆ dom
𝑆) → ((𝑆 “ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)}))) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
252 | 246, 250,
251 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
253 | 244, 252 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
254 | 233, 253 | sstrid 3912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
255 | 254 | unissd 4829 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) |
256 | | df-ov 7216 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑥)𝑆𝑗) = (𝑆‘〈(1st ‘𝑥), 𝑗〉) |
257 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
258 | | elrelimasn 5953 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
𝐴 → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) |
259 | 66, 258 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) |
260 | 259 | biimpa 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (1st
‘𝑥)𝐴𝑗) |
261 | | df-br 5054 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝐴𝑗 ↔ 〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) |
262 | 260, 261 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) →
〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) |
263 | 257, 262 | ffvelrnd 6905 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (𝑆‘〈(1st ‘𝑥), 𝑗〉) ∈ (SubGrp‘𝐺)) |
264 | 256, 263 | eqeltrid 2842 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → ((1st
‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺)) |
265 | 264 | fmpttd 6932 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)):(𝐴 “ {(1st ‘𝑥)})⟶(SubGrp‘𝐺)) |
266 | 265 | frnd 6553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺)) |
267 | 266, 207 | sstrd 3911 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺)) |
268 | | sspwuni 5008 |
. . . . . . . . . 10
⊢ (ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) |
269 | 267, 268 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) |
270 | 166, 3, 255, 269 | mrcssd 17127 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
271 | 3 | dprdspan 19414 |
. . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
272 | 53, 271 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
273 | 270, 272 | sseqtrrd 3942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
274 | 16, 17 | fnmpti 6521 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 |
275 | | fnressn 6973 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) |
276 | 274, 52, 275 | sylancr 590 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) |
277 | 124 | opeq2d 4791 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉 = 〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉) |
278 | 277 | sneqd 4553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉} =
{〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) |
279 | 276, 278 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) |
280 | 279 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉})) |
281 | | dprdsubg 19411 |
. . . . . . . . . . . . 13
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) |
282 | 53, 281 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) |
283 | | dprdsn 19423 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
284 | 52, 282, 283 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
285 | 284 | simprd 499 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
286 | 280, 285 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
287 | 4 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
288 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
289 | | difss 4046 |
. . . . . . . . . . 11
⊢ (𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 |
290 | 289 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1st ‘𝑥)}) ⊆ 𝐼) |
291 | | disjdif 4386 |
. . . . . . . . . . 11
⊢
({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅ |
292 | 291 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅) |
293 | 287, 288,
169, 290, 292, 1 | dprdcntz2 19425 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
294 | 286, 293 | eqsstrrd 3940 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
295 | 29 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
296 | 66, 245, 49, 295, 287, 3, 290 | dprd2dlem1 19428 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
297 | | resmpt 5905 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
298 | 289, 297 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
299 | 298 | oveq2i 7224 |
. . . . . . . . . 10
⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
300 | 296, 299 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
301 | 300 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
302 | 294, 301 | sseqtrrd 3942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
303 | 273, 302 | sstrd 3911 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
304 | 225, 1 | lsmsubg 19043 |
. . . . . 6
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺) ∧
(𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) |
305 | 222, 224,
303, 304 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) |
306 | 3 | mrcsscl 17123 |
. . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∧ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) →
(𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
307 | 166, 228,
305, 306 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
308 | | sslin 4149 |
. . . 4
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) |
309 | 307, 308 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) |
310 | 41 | ffvelrnda 6904 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
311 | 225 | lsmlub 19054 |
. . . . . . . . . 10
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
312 | 222, 310,
282, 311 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
313 | 273, 121,
312 | mpbi2and 712 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
314 | 313, 124 | sseqtrrd 3942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
315 | 287, 288,
290 | dprdres 19415 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))) |
316 | 315 | simpld 498 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
317 | 3 | dprdspan 19414 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
318 | 316, 317 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
319 | | df-ima 5564 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) |
320 | 319 | unieqi 4832 |
. . . . . . . . . . 11
⊢ ∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) |
321 | 320 | fveq2i 6720 |
. . . . . . . . . 10
⊢ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
322 | 318, 321 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
323 | 300, 322 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
324 | | eqimss 3957 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) = (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
325 | 323, 324 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
326 | | ss2in 4151 |
. . . . . . 7
⊢ ((((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) → (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) |
327 | 314, 325,
326 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) |
328 | 287, 288,
52, 2, 3 | dprddisj 19396 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) =
{(0g‘𝐺)}) |
329 | 327, 328 | sseqtrd 3941 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆
{(0g‘𝐺)}) |
330 | 225 | lsmub2 19047 |
. . . . . . . . 9
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
331 | 222, 310,
330 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
332 | 2 | subg0cl 18551 |
. . . . . . . . 9
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
333 | 310, 332 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
334 | 331, 333 | sseldd 3902 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
335 | 2 | subg0cl 18551 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ∈
(SubGrp‘𝐺) →
(0g‘𝐺)
∈ (𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))))) |
336 | 224, 335 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
337 | 334, 336 | elind 4108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
338 | 337 | snssd 4722 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
339 | 329, 338 | eqssd 3918 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) =
{(0g‘𝐺)}) |
340 | | incom 4115 |
. . . . 5
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
341 | 69, 101 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
342 | 61 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
343 | 99, 341, 342 | 3eqtr4a 2804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
344 | | eqimss2 3958 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) |
345 | 343, 344 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) |
346 | | eldifsn 4700 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) |
347 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴) |
348 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)})) |
349 | 247, 348 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴) |
350 | 347, 349,
74 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
351 | 350 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
352 | 351, 109 | eqtr4di 2796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) |
353 | 350, 348 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st
‘𝑥)})) |
354 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘𝑦) ∈ V |
355 | 354 | opelresi 5859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ↔ ((1st
‘𝑦) ∈
{(1st ‘𝑥)}
∧ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴)) |
356 | 355 | simplbi 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) → (1st
‘𝑦) ∈
{(1st ‘𝑥)}) |
357 | 353, 356 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) ∈ {(1st
‘𝑥)}) |
358 | | elsni 4558 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑦) ∈ {(1st ‘𝑥)} → (1st
‘𝑦) = (1st
‘𝑥)) |
359 | 357, 358 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) = (1st ‘𝑥)) |
360 | 359 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑦)𝑆(2nd ‘𝑦)) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
361 | 352, 360 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
362 | 348, 230 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) |
363 | | xp2nd 7794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) →
(2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)})) |
364 | 362, 363 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑥)})) |
365 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥) |
366 | 61 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
367 | 350, 366 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉)) |
368 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑦) ∈ V |
369 | 368, 354 | opth 5360 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ↔ ((1st
‘𝑦) = (1st
‘𝑥) ∧
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
370 | 369 | baib 539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝑦) = (1st ‘𝑥) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
371 | 359, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
372 | 367, 371 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2nd ‘𝑦) = (2nd ‘𝑥))) |
373 | 372 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) |
374 | 365, 373 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ≠ (2nd
‘𝑥)) |
375 | | eldifsn 4700 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↔
((2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)}) ∧ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) |
376 | 364, 374,
375 | sylanbrc 586 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) |
377 | | ovex 7246 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V |
378 | | difss 4046 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) |
379 | | resmpt 5905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) |
380 | 378, 379 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) |
381 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
382 | 380, 381 | elrnmpt1s 5826 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ∧
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V) → ((1st
‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
383 | 376, 377,
382 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
384 | 361, 383 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
385 | | df-ima 5564 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) |
386 | 384, 385 | eleqtrrdi 2849 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
387 | 386 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
388 | 346, 387 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
389 | 388 | ralrimiv 3104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
390 | 231, 250 | sstrid 3912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) |
391 | | funimass4 6777 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑆 ∧ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
392 | 246, 390,
391 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
393 | 389, 392 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
394 | 393 | unissd 4829 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
395 | | imassrn 5940 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) |
396 | 395, 267 | sstrid 3912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)) |
397 | | sspwuni 5008 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)
↔ ∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) |
398 | 396, 397 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) |
399 | 166, 3, 394, 398 | mrcssd 17127 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
400 | | ss2in 4151 |
. . . . . . . 8
⊢ (((𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) →
((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) |
401 | 345, 399,
400 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) |
402 | 58 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) |
403 | 53, 402, 69, 2, 3 | dprddisj 19396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) =
{(0g‘𝐺)}) |
404 | 401, 403 | sseqtrd 3941 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
405 | 2 | subg0cl 18551 |
. . . . . . . . 9
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
406 | 222, 405 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
407 | 333, 406 | elind 4108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) |
408 | 407 | snssd 4722 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) |
409 | 404, 408 | eqssd 3918 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) = {(0g‘𝐺)}) |
410 | 340, 409 | syl5eq 2790 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0g‘𝐺)}) |
411 | 225, 222,
310, 224, 2, 339, 410 | lsmdisj2 19072 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) =
{(0g‘𝐺)}) |
412 | 309, 411 | sseqtrd 3941 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
413 | 1, 2, 3, 6, 40, 41, 162, 412 | dmdprdd 19386 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |