Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | eqid 2610 |
. 2
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | dprd2d.k |
. 2
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
4 | | dprd2d.5 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
5 | | dprdgrp 18227 |
. . 3
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | resiun2 5338 |
. . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = ∪
𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) |
8 | | iunid 4511 |
. . . . . 6
⊢ ∪ 𝑖 ∈ 𝐼 {𝑖} = 𝐼 |
9 | 8 | reseq2i 5314 |
. . . . 5
⊢ (𝐴 ↾ ∪ 𝑖 ∈ 𝐼 {𝑖}) = (𝐴 ↾ 𝐼) |
10 | 7, 9 | eqtr3i 2634 |
. . . 4
⊢ ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = (𝐴 ↾ 𝐼) |
11 | | dprd2d.1 |
. . . . 5
⊢ (𝜑 → Rel 𝐴) |
12 | | dprd2d.3 |
. . . . 5
⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) |
13 | | relssres 5357 |
. . . . 5
⊢ ((Rel
𝐴 ∧ dom 𝐴 ⊆ 𝐼) → (𝐴 ↾ 𝐼) = 𝐴) |
14 | 11, 12, 13 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐴 ↾ 𝐼) = 𝐴) |
15 | 10, 14 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) = 𝐴) |
16 | | ovex 6577 |
. . . . . 6
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) ∈ V |
17 | | eqid 2610 |
. . . . . 6
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
18 | 16, 17 | dmmpti 5936 |
. . . . 5
⊢ dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼 |
19 | | reldmdprd 18219 |
. . . . . . 7
⊢ Rel dom
DProd |
20 | 19 | brrelex2i 5083 |
. . . . . 6
⊢ (𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) → (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
21 | | dmexg 6989 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
22 | 4, 20, 21 | 3syl 18 |
. . . . 5
⊢ (𝜑 → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ∈ V) |
23 | 18, 22 | syl5eqelr 2693 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
24 | | ressn 5588 |
. . . . . 6
⊢ (𝐴 ↾ {𝑖}) = ({𝑖} × (𝐴 “ {𝑖})) |
25 | | snex 4835 |
. . . . . . 7
⊢ {𝑖} ∈ V |
26 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑖𝑆𝑗) ∈ V |
27 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) |
28 | 26, 27 | dmmpti 5936 |
. . . . . . . 8
⊢ dom
(𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝐴 “ {𝑖}) |
29 | | dprd2d.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
30 | 19 | brrelex2i 5083 |
. . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
31 | | dmexg 6989 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → dom (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ∈ V) |
33 | 28, 32 | syl5eqelr 2693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 “ {𝑖}) ∈ V) |
34 | | xpexg 6858 |
. . . . . . 7
⊢ (({𝑖} ∈ V ∧ (𝐴 “ {𝑖}) ∈ V) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) |
35 | 25, 33, 34 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ({𝑖} × (𝐴 “ {𝑖})) ∈ V) |
36 | 24, 35 | syl5eqel 2692 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐴 ↾ {𝑖}) ∈ V) |
37 | 36 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
38 | | iunexg 7035 |
. . . 4
⊢ ((𝐼 ∈ V ∧ ∀𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
39 | 23, 37, 38 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ 𝐼 (𝐴 ↾ {𝑖}) ∈ V) |
40 | 15, 39 | eqeltrrd 2689 |
. 2
⊢ (𝜑 → 𝐴 ∈ V) |
41 | | dprd2d.2 |
. 2
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
42 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝐴 ⊆ 𝐼) |
43 | | 1stdm 7106 |
. . . . . . . . . 10
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
44 | 11, 43 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
45 | 42, 44 | sseldd 3569 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ 𝐼) |
46 | 29 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
48 | | sneq 4135 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑥) → {𝑖} = {(1st ‘𝑥)}) |
49 | 48 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑥)})) |
50 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑥) → (𝑖𝑆𝑗) = ((1st ‘𝑥)𝑆𝑗)) |
51 | 49, 50 | mpteq12dv 4663 |
. . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑥) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
52 | 51 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
53 | 52 | rspcv 3278 |
. . . . . . . 8
⊢
((1st ‘𝑥) ∈ 𝐼 → (∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
54 | 45, 47, 53 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
55 | 54 | 3ad2antr1 1219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
56 | 55 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
57 | | ovex 6577 |
. . . . . . 7
⊢
((1st ‘𝑥)𝑆𝑗) ∈ V |
58 | | eqid 2610 |
. . . . . . 7
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) |
59 | 57, 58 | dmmpti 5936 |
. . . . . 6
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)}) |
60 | 59 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) |
61 | | 1st2nd 7105 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
62 | 11, 61 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
63 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
64 | 62, 63 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) |
65 | | df-br 4584 |
. . . . . . . . 9
⊢
((1st ‘𝑥)𝐴(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐴) |
66 | 64, 65 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥)𝐴(2nd ‘𝑥)) |
67 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Rel 𝐴) |
68 | | elrelimasn 5408 |
. . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)}) ↔
(1st ‘𝑥)𝐴(2nd ‘𝑥))) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴(2nd ‘𝑥))) |
70 | 66, 69 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) |
71 | 70 | 3ad2antr1 1219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)})) |
72 | 71 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ∈ (𝐴 “ {(1st
‘𝑥)})) |
73 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → Rel 𝐴) |
74 | | simpr2 1061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐴) |
75 | | 1st2nd 7105 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
76 | 73, 74, 75 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
77 | 76, 74 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) |
78 | | df-br 4584 |
. . . . . . . . 9
⊢
((1st ‘𝑦)𝐴(2nd ‘𝑦) ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴) |
79 | 77, 78 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦)𝐴(2nd ‘𝑦)) |
80 | | elrelimasn 5408 |
. . . . . . . . 9
⊢ (Rel
𝐴 → ((2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)}) ↔
(1st ‘𝑦)𝐴(2nd ‘𝑦))) |
81 | 73, 80 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) ↔ (1st
‘𝑦)𝐴(2nd ‘𝑦))) |
82 | 79, 81 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)})) |
83 | 82 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑦)})) |
84 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (1st
‘𝑥) = (1st
‘𝑦)) |
85 | 84 | sneqd 4137 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → {(1st
‘𝑥)} =
{(1st ‘𝑦)}) |
86 | 85 | imaeq2d 5385 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝐴 “ {(1st ‘𝑥)}) = (𝐴 “ {(1st ‘𝑦)})) |
87 | 83, 86 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑦) ∈ (𝐴 “ {(1st
‘𝑥)})) |
88 | | simplr3 1098 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → 𝑥 ≠ 𝑦) |
89 | | simpr1 1060 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐴) |
90 | 73, 89, 61 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
91 | 90, 76 | eqeq12d 2625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉)) |
92 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V |
93 | | fvex 6113 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
94 | 92, 93 | opth 4871 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥) =
(2nd ‘𝑦))) |
95 | 91, 94 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑥 = 𝑦 ↔ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) = (2nd
‘𝑦)))) |
96 | 95 | baibd 946 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 = 𝑦 ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
97 | 96 | necon3bid 2826 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑥 ≠ 𝑦 ↔ (2nd ‘𝑥) ≠ (2nd
‘𝑦))) |
98 | 88, 97 | mpbid 221 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (2nd
‘𝑥) ≠
(2nd ‘𝑦)) |
99 | 56, 60, 72, 87, 98, 1 | dprdcntz 18230 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)))) |
100 | | df-ov 6552 |
. . . . . 6
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥)) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
101 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑗 = (2nd ‘𝑥) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑥))) |
102 | 101, 58, 57 | fvmpt3i 6196 |
. . . . . . 7
⊢
((2nd ‘𝑥) ∈ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
103 | 71, 102 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
104 | 90 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
105 | 100, 103,
104 | 3eqtr4a 2670 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
106 | 105 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
107 | 84 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) |
108 | 86, 107 | mpteq12dv 4663 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
109 | 108 | fveq1d 6105 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦))) |
110 | | df-ov 6552 |
. . . . . . . 8
⊢
((1st ‘𝑦)𝑆(2nd ‘𝑦)) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
111 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑦)𝑆𝑗) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) |
112 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) |
113 | | ovex 6577 |
. . . . . . . . . 10
⊢
((1st ‘𝑦)𝑆𝑗) ∈ V |
114 | 111, 112,
113 | fvmpt3i 6196 |
. . . . . . . . 9
⊢
((2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑦)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) |
115 | 82, 114 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = ((1st
‘𝑦)𝑆(2nd ‘𝑦))) |
116 | 76 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
117 | 110, 115,
116 | 3eqtr4a 2670 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
118 | 117 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
119 | 109, 118 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦)) = (𝑆‘𝑦)) |
120 | 119 | fveq2d 6107 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → ((Cntz‘𝐺)‘((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑦))) = ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
121 | 99, 106, 120 | 3sstr3d 3610 |
. . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) = (1st ‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
122 | 11, 41, 12, 29, 4, 3 | dprd2dlem2 18262 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
123 | 51 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑖 = (1st ‘𝑥) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
124 | 123, 17, 16 | fvmpt3i 6196 |
. . . . . . . 8
⊢
((1st ‘𝑥) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
125 | 45, 124 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
126 | 122, 125 | sseqtr4d 3605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
127 | 126 | 3ad2antr1 1219 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
128 | 127 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
129 | 4 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
130 | 18 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → dom
(𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
131 | 45 | 3ad2antr1 1219 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑥) ∈ 𝐼) |
132 | 131 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
∈ 𝐼) |
133 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom 𝐴 ⊆ 𝐼) |
134 | | 1stdm 7106 |
. . . . . . . . 9
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ dom 𝐴) |
135 | 73, 74, 134 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ dom 𝐴) |
136 | 133, 135 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (1st ‘𝑦) ∈ 𝐼) |
137 | 136 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑦)
∈ 𝐼) |
138 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
(1st ‘𝑥)
≠ (1st ‘𝑦)) |
139 | 129, 130,
132, 137, 138, 1 | dprdcntz 18230 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)))) |
140 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (1st ‘𝑦) → {𝑖} = {(1st ‘𝑦)}) |
141 | 140 | imaeq2d 5385 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st ‘𝑦)})) |
142 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝑖𝑆𝑗) = ((1st ‘𝑦)𝑆𝑗)) |
143 | 141, 142 | mpteq12dv 4663 |
. . . . . . . . . . 11
⊢ (𝑖 = (1st ‘𝑦) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
144 | 143 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑖 = (1st ‘𝑦) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
145 | 144, 17, 16 | fvmpt3i 6196 |
. . . . . . . . 9
⊢
((1st ‘𝑦) ∈ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
146 | 136, 145 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦)) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
147 | 146 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) = ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))))) |
148 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
149 | 148 | dprdssv 18238 |
. . . . . . . 8
⊢ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) |
150 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
151 | 143 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑖 = (1st ‘𝑦) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
152 | 151 | rspcv 3278 |
. . . . . . . . . . 11
⊢
((1st ‘𝑦) ∈ 𝐼 → (∀𝑖 ∈ 𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
153 | 136, 150,
152 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) |
154 | 113, 112 | dmmpti 5936 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ (𝐴 “ {(1st
‘𝑦)}) ↦
((1st ‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)}) |
155 | 154 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑦)})) |
156 | 153, 155,
82 | dprdub 18247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))‘(2nd ‘𝑦)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
157 | 117, 156 | eqsstr3d 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) |
158 | 148, 1 | cntz2ss 17588 |
. . . . . . . 8
⊢ (((𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗))) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑦) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
159 | 149, 157,
158 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘(𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑦)}) ↦ ((1st
‘𝑦)𝑆𝑗)))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
160 | 147, 159 | eqsstrd 3602 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
161 | 160 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) →
((Cntz‘𝐺)‘((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑦))) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
162 | 139, 161 | sstrd 3578 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
163 | 128, 162 | sstrd 3578 |
. . 3
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) ∧ (1st ‘𝑥) ≠ (1st
‘𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
164 | 121, 163 | pm2.61dane 2869 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
165 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 ∈ Grp) |
166 | 148 | subgacs 17452 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
167 | | acsmre 16136 |
. . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
168 | 165, 166,
167 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
169 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = 𝐴) |
170 | | undif2 3996 |
. . . . . . . . . . . . . . . . . 18
⊢
({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})) = ({(1st
‘𝑥)} ∪ 𝐼) |
171 | 45 | snssd 4281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(1st ‘𝑥)} ⊆ 𝐼) |
172 | | ssequn1 3745 |
. . . . . . . . . . . . . . . . . . 19
⊢
({(1st ‘𝑥)} ⊆ 𝐼 ↔ ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) |
173 | 171, 172 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∪ 𝐼) = 𝐼) |
174 | 170, 173 | syl5req 2657 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐼 = ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)}))) |
175 | 174 | reseq2d 5317 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ 𝐼) = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) |
176 | 169, 175 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = (𝐴 ↾ ({(1st ‘𝑥)} ∪ (𝐼 ∖ {(1st ‘𝑥)})))) |
177 | | resundi 5330 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ ({(1st
‘𝑥)} ∪ (𝐼 ∖ {(1st
‘𝑥)}))) = ((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
178 | 176, 177 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = ((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
179 | 178 | difeq1d 3689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥})) |
180 | | difundir 3839 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
181 | 179, 180 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}))) |
182 | | neirr 2791 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(1st ‘𝑥)
≠ (1st ‘𝑥) |
183 | 62 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ↔
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
184 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∈
(𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) |
185 | 93 | brres 5323 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) ↔ ((1st
‘𝑥)𝐴(2nd ‘𝑥) ∧ (1st ‘𝑥) ∈ (𝐼 ∖ {(1st ‘𝑥)}))) |
186 | 185 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ∈ (𝐼 ∖ {(1st
‘𝑥)})) |
187 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑥) ∈ (𝐼 ∖ {(1st ‘𝑥)}) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
188 | 186, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑥)(𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))(2nd ‘𝑥) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
189 | 184, 188 | sylbir 224 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥)) |
190 | 183, 189 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (1st
‘𝑥) ≠
(1st ‘𝑥))) |
191 | 182, 190 | mtoi 189 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
192 | | disjsn 4192 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
193 | 191, 192 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅) |
194 | | disj3 3973 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∩ {𝑥}) = ∅ ↔ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
195 | 193, 194 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) = ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) |
196 | 195 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥}) = (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
197 | 196 | uneq2d 3729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ ((𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∖ {𝑥})) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
198 | 181, 197 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) = (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
199 | 198 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
200 | | imaundi 5464 |
. . . . . . . . . 10
⊢ (𝑆 “ (((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ∪ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
201 | 199, 200 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) = ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
202 | 201 | unieqd 4382 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = ∪ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
203 | | uniun 4392 |
. . . . . . . 8
⊢ ∪ ((𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
204 | 202, 203 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) = (∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
205 | | imassrn 5396 |
. . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran 𝑆 |
206 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
207 | 41, 206 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
208 | 207 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
209 | | mresspw 16075 |
. . . . . . . . . . . . 13
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
210 | 168, 209 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
211 | 208, 210 | sstrd 3578 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
212 | 205, 211 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
213 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) |
214 | 212, 213 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) |
215 | 168, 3, 214 | mrcssidd 16108 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
216 | | imassrn 5396 |
. . . . . . . . . . 11
⊢ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ ran 𝑆 |
217 | 216, 211 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺)) |
218 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ ((𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ 𝒫
(Base‘𝐺) ↔ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))) ⊆
(Base‘𝐺)) |
219 | 217, 218 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) |
220 | 168, 3, 219 | mrcssidd 16108 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
221 | | unss12 3747 |
. . . . . . . 8
⊢ ((∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∧ ∪
(𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → (∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
222 | 215, 220,
221 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪
(𝑆 “ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})) ∪ ∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ⊆
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
223 | 204, 222 | eqsstrd 3602 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
224 | 3 | mrccl 16094 |
. . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
225 | 168, 214,
224 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
226 | 3 | mrccl 16094 |
. . . . . . . 8
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) |
227 | 168, 219,
226 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) |
228 | | eqid 2610 |
. . . . . . . 8
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
229 | 228 | lsmunss 17896 |
. . . . . . 7
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺)) →
((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
230 | 225, 227,
229 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∪ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
231 | 223, 230 | sstrd 3578 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
232 | | difss 3699 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ (𝐴 ↾ {(1st ‘𝑥)}) |
233 | | ressn 5588 |
. . . . . . . . . . . . 13
⊢ (𝐴 ↾ {(1st
‘𝑥)}) =
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) |
234 | 232, 233 | sseqtri 3600 |
. . . . . . . . . . . 12
⊢ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) |
235 | | imass2 5420 |
. . . . . . . . . . . 12
⊢ (((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥}) ⊆ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})))) |
236 | 234, 235 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) |
237 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝑆𝑖) ∈ V |
238 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → ((1st ‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆𝑖)) |
239 | 58, 238 | elrnmpt1s 5294 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) ∧ ((1st
‘𝑥)𝑆𝑖) ∈ V) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
240 | 237, 239 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝐴 “ {(1st ‘𝑥)}) → ((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
241 | 240 | rgen 2906 |
. . . . . . . . . . . . . 14
⊢
∀𝑖 ∈
(𝐴 “ {(1st
‘𝑥)})((1st
‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) |
242 | 241 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
243 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (1st ‘𝑥) → (𝑦𝑆𝑖) = ((1st ‘𝑥)𝑆𝑖)) |
244 | 243 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (1st ‘𝑥) → ((𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
245 | 244 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1st ‘𝑥) → (∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
246 | 92, 245 | ralsn 4169 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
{(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})((1st ‘𝑥)𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
247 | 242, 246 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
248 | 41 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
249 | | ffun 5961 |
. . . . . . . . . . . . . 14
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → Fun 𝑆) |
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun 𝑆) |
251 | | resss 5342 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ↾ {(1st
‘𝑥)}) ⊆ 𝐴 |
252 | 233, 251 | eqsstr3i 3599 |
. . . . . . . . . . . . . 14
⊢
({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ 𝐴 |
253 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝑆:𝐴⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐴) |
254 | 248, 253 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐴) |
255 | 252, 254 | syl5sseqr 3617 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)})) ⊆ dom 𝑆) |
256 | | funimassov 6709 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑆 ∧ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) ⊆ dom
𝑆) → ((𝑆 “ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)}))) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
257 | 250, 255,
256 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↔ ∀𝑦 ∈ {(1st ‘𝑥)}∀𝑖 ∈ (𝐴 “ {(1st ‘𝑥)})(𝑦𝑆𝑖) ∈ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
258 | 247, 257 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
259 | 236, 258 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) |
260 | 259 | unissd 4398 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) |
261 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑥)𝑆𝑗) = (𝑆‘〈(1st ‘𝑥), 𝑗〉) |
262 | 41 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
263 | | elrelimasn 5408 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
𝐴 → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) |
264 | 67, 263 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↔ (1st
‘𝑥)𝐴𝑗)) |
265 | 264 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (1st
‘𝑥)𝐴𝑗) |
266 | | df-br 4584 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑥)𝐴𝑗 ↔ 〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) |
267 | 265, 266 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) →
〈(1st ‘𝑥), 𝑗〉 ∈ 𝐴) |
268 | 262, 267 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → (𝑆‘〈(1st ‘𝑥), 𝑗〉) ∈ (SubGrp‘𝐺)) |
269 | 261, 268 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ (𝐴 “ {(1st ‘𝑥)})) → ((1st
‘𝑥)𝑆𝑗) ∈ (SubGrp‘𝐺)) |
270 | 269, 58 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)):(𝐴 “ {(1st ‘𝑥)})⟶(SubGrp‘𝐺)) |
271 | | frn 5966 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)):(𝐴 “ {(1st ‘𝑥)})⟶(SubGrp‘𝐺) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺)) |
272 | 270, 271 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (SubGrp‘𝐺)) |
273 | 272, 210 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺)) |
274 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ (ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ran (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) |
275 | 273, 274 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) ⊆ (Base‘𝐺)) |
276 | 168, 3, 260, 275 | mrcssd 16107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
277 | 3 | dprdspan 18249 |
. . . . . . . . 9
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
278 | 54, 277 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) = (𝐾‘∪ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)))) |
279 | 276, 278 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
280 | 16, 17 | fnmpti 5935 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 |
281 | | fnressn 6330 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) Fn 𝐼 ∧ (1st ‘𝑥) ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) |
282 | 280, 45, 281 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉}) |
283 | 125 | opeq2d 4347 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉 = 〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉) |
284 | 283 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {〈(1st ‘𝑥), ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))〉} =
{〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) |
285 | 282, 284 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)}) = {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) |
286 | 285 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉})) |
287 | | dprdsubg 18246 |
. . . . . . . . . . . . 13
⊢ (𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) |
288 | 54, 287 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) |
289 | | dprdsn 18258 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑥) ∈ 𝐼 ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
290 | 45, 288, 289 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd {〈(1st
‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉} ∧ (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
291 | 290 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd {〈(1st ‘𝑥), (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))〉}) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
292 | 286, 291 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) = (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
293 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
294 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) = 𝐼) |
295 | | difss 3699 |
. . . . . . . . . . 11
⊢ (𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 |
296 | 295 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐼 ∖ {(1st ‘𝑥)}) ⊆ 𝐼) |
297 | | disjdif 3992 |
. . . . . . . . . . 11
⊢
({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅ |
298 | 297 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({(1st ‘𝑥)} ∩ (𝐼 ∖ {(1st ‘𝑥)})) = ∅) |
299 | 293, 294,
171, 296, 298, 1 | dprdcntz2 18260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ {(1st ‘𝑥)})) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
300 | 292, 299 | eqsstr3d 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
301 | 29 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) |
302 | 67, 248, 42, 301, 293, 3, 296 | dprd2dlem1 18263 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) |
303 | | resmpt 5369 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∖ {(1st
‘𝑥)}) ⊆ 𝐼 → ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
304 | 295, 303 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) = (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) |
305 | 304 | oveq2i 6560 |
. . . . . . . . . 10
⊢ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐺 DProd (𝑖 ∈ (𝐼 ∖ {(1st ‘𝑥)}) ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) |
306 | 302, 305 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
307 | 306 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) = ((Cntz‘𝐺)‘(𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
308 | 300, 307 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
309 | 279, 308 | sstrd 3578 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
310 | 228, 1 | lsmsubg 17892 |
. . . . . 6
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ∈
(SubGrp‘𝐺) ∧
(𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ ((Cntz‘𝐺)‘(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) → ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) |
311 | 225, 227,
309, 310 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) |
312 | 3 | mrcsscl 16103 |
. . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∧ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ∈
(SubGrp‘𝐺)) →
(𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
313 | 168, 231,
311, 312 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
314 | | sslin 3801 |
. . . 4
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ∖ {𝑥}))) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) |
315 | 313, 314 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))))) |
316 | 41 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
317 | 228 | lsmlub 17901 |
. . . . . . . . . 10
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∈ (SubGrp‘𝐺)) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
318 | 225, 316,
288, 317 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))) ∧ (𝑆‘𝑥) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) ↔ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))))) |
319 | 279, 122,
318 | mpbi2and 958 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)))) |
320 | 319, 125 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥))) |
321 | 293, 294,
296 | dprdres 18250 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) ∧ (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) ⊆ (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))))) |
322 | 321 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
323 | 3 | dprdspan 18249 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
324 | 322, 323 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})))) |
325 | | df-ima 5051 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) |
326 | 325 | unieqi 4381 |
. . . . . . . . . . 11
⊢ ∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})) = ∪ ran ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)})) |
327 | 326 | fveq2i 6106 |
. . . . . . . . . 10
⊢ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ran
((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) |
328 | 324, 327 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺 DProd ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) ↾ (𝐼 ∖ {(1st ‘𝑥)}))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
329 | 306, 328 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) = (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
330 | | eqimss 3620 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) = (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
331 | 329, 330 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) |
332 | | ss2in 3802 |
. . . . . . 7
⊢ ((((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ⊆ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))) ⊆ (𝐾‘∪ ((𝑖
∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) → (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) |
333 | 320, 331,
332 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆ (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)}))))) |
334 | 293, 294,
45, 2, 3 | dprddisj 18231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))‘(1st ‘𝑥)) ∩ (𝐾‘∪ ((𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))) “ (𝐼 ∖ {(1st ‘𝑥)})))) =
{(0g‘𝐺)}) |
335 | 333, 334 | sseqtrd 3604 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) ⊆
{(0g‘𝐺)}) |
336 | 228 | lsmub2 17895 |
. . . . . . . . 9
⊢ (((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
337 | 225, 316,
336 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
338 | 2 | subg0cl 17425 |
. . . . . . . . 9
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
339 | 316, 338 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
340 | 337, 339 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥))) |
341 | 2 | subg0cl 17425 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)})))) ∈
(SubGrp‘𝐺) →
(0g‘𝐺)
∈ (𝐾‘∪ (𝑆
“ (𝐴 ↾ (𝐼 ∖ {(1st
‘𝑥)}))))) |
342 | 227, 341 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) |
343 | 340, 342 | elind 3760 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
344 | 343 | snssd 4281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) |
345 | 335, 344 | eqssd 3585 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝑆‘𝑥)) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)}))))) =
{(0g‘𝐺)}) |
346 | | incom 3767 |
. . . . 5
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
347 | 70, 102 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = ((1st
‘𝑥)𝑆(2nd ‘𝑥))) |
348 | 62 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) = (𝑆‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
349 | 100, 347,
348 | 3eqtr4a 2670 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥)) |
350 | | eqimss2 3621 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) = (𝑆‘𝑥) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) |
351 | 349, 350 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥))) |
352 | | eldifsn 4260 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) |
353 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → Rel 𝐴) |
354 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)})) |
355 | 251, 354 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ 𝐴) |
356 | 353, 355,
75 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
357 | 356 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = (𝑆‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
358 | 357, 110 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑦)𝑆(2nd ‘𝑦))) |
359 | 356, 354 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st
‘𝑥)})) |
360 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘𝑦) ∈ V |
361 | 360 | opelres 5322 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ↔
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ 𝐴 ∧ (1st ‘𝑦) ∈ {(1st
‘𝑥)})) |
362 | 361 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ (𝐴 ↾ {(1st ‘𝑥)}) → (1st
‘𝑦) ∈
{(1st ‘𝑥)}) |
363 | 359, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) ∈ {(1st
‘𝑥)}) |
364 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑦) ∈ {(1st ‘𝑥)} → (1st
‘𝑦) = (1st
‘𝑥)) |
365 | 363, 364 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (1st ‘𝑦) = (1st ‘𝑥)) |
366 | 365 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑦)𝑆(2nd ‘𝑦)) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
367 | 358, 366 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
368 | 354, 233 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ∈ ({(1st ‘𝑥)} × (𝐴 “ {(1st ‘𝑥)}))) |
369 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ({(1st
‘𝑥)} × (𝐴 “ {(1st
‘𝑥)})) →
(2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)})) |
370 | 368, 369 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ (𝐴 “ {(1st ‘𝑥)})) |
371 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑦 ≠ 𝑥) |
372 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
373 | 356, 372 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉)) |
374 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑦) ∈ V |
375 | 374, 360 | opth 4871 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ↔ ((1st
‘𝑦) = (1st
‘𝑥) ∧
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
376 | 375 | baib 942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝑦) = (1st ‘𝑥) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
377 | 365, 376 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (〈(1st ‘𝑦), (2nd ‘𝑦)〉 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ↔
(2nd ‘𝑦) =
(2nd ‘𝑥))) |
378 | 373, 377 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 = 𝑥 ↔ (2nd ‘𝑦) = (2nd ‘𝑥))) |
379 | 378 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑦 ≠ 𝑥 ↔ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) |
380 | 371, 379 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ≠ (2nd
‘𝑥)) |
381 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↔
((2nd ‘𝑦)
∈ (𝐴 “
{(1st ‘𝑥)}) ∧ (2nd ‘𝑦) ≠ (2nd
‘𝑥))) |
382 | 370, 380,
381 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) |
383 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V |
384 | | difss 3699 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) |
385 | | resmpt 5369 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 “ {(1st
‘𝑥)}) ∖
{(2nd ‘𝑥)}) ⊆ (𝐴 “ {(1st ‘𝑥)}) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗))) |
386 | 384, 385 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = (𝑗 ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) |
387 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (2nd ‘𝑦) → ((1st
‘𝑥)𝑆𝑗) = ((1st ‘𝑥)𝑆(2nd ‘𝑦))) |
388 | 386, 387 | elrnmpt1s 5294 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑦) ∈ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}) ∧
((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ V) → ((1st
‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
389 | 382, 383,
388 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → ((1st ‘𝑥)𝑆(2nd ‘𝑦)) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
390 | 367, 389 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
391 | | df-ima 5051 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) = ran ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) ↾ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) |
392 | 390, 391 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥)) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
393 | 392 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑦 ∈ (𝐴 ↾ {(1st ‘𝑥)}) ∧ 𝑦 ≠ 𝑥) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
394 | 352, 393 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) → (𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
395 | 394 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
396 | 234, 255 | syl5ss 3579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) |
397 | | funimass4 6157 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑆 ∧ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}) ⊆ dom 𝑆) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
398 | 250, 396,
397 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ↔
∀𝑦 ∈ ((𝐴 ↾ {(1st
‘𝑥)}) ∖ {𝑥})(𝑆‘𝑦) ∈ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
399 | 395, 398 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
400 | 399 | unissd 4398 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})) ⊆ ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))) |
401 | | imassrn 5396 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆ ran
(𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) |
402 | 401, 273 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)) |
403 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
𝒫 (Base‘𝐺)
↔ ∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) |
404 | 402, 403 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
((𝑗 ∈ (𝐴 “ {(1st
‘𝑥)}) ↦
((1st ‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})) ⊆
(Base‘𝐺)) |
405 | 168, 3, 400, 404 | mrcssd 16107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) |
406 | | ss2in 3802 |
. . . . . . . 8
⊢ (((𝑆‘𝑥) ⊆ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∧ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ⊆ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) →
((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) |
407 | 351, 405,
406 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)}))))) |
408 | 59 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) = (𝐴 “ {(1st ‘𝑥)})) |
409 | 54, 408, 70, 2, 3 | dprddisj 18231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗))‘(2nd ‘𝑥)) ∩ (𝐾‘∪ ((𝑗 ∈ (𝐴 “ {(1st ‘𝑥)}) ↦ ((1st
‘𝑥)𝑆𝑗)) “ ((𝐴 “ {(1st ‘𝑥)}) ∖ {(2nd
‘𝑥)})))) =
{(0g‘𝐺)}) |
410 | 407, 409 | sseqtrd 3604 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
411 | 2 | subg0cl 17425 |
. . . . . . . . 9
⊢ ((𝐾‘∪ (𝑆
“ ((𝐴 ↾
{(1st ‘𝑥)}) ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
412 | 225, 411 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) |
413 | 339, 412 | elind 3760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) |
414 | 413 | snssd 4281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))))) |
415 | 410, 414 | eqssd 3585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))) = {(0g‘𝐺)}) |
416 | 346, 415 | syl5eq 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥}))) ∩ (𝑆‘𝑥)) = {(0g‘𝐺)}) |
417 | 228, 225,
316, 227, 2, 345, 416 | lsmdisj2 17918 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((𝐾‘∪ (𝑆 “ ((𝐴 ↾ {(1st ‘𝑥)}) ∖ {𝑥})))(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐴 ↾ (𝐼 ∖ {(1st ‘𝑥)})))))) =
{(0g‘𝐺)}) |
418 | 315, 417 | sseqtrd 3604 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐴 ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
419 | 1, 2, 3, 6, 40, 41, 164, 418 | dmdprdd 18221 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |