Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | dprd0.0 |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | eqid 2622 |
. . 3
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
4 | | simpl 473 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝐺 ∈ Grp) |
5 | | simpr 477 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ 𝑉) |
6 | 2 | 0subg 17619 |
. . . . 5
⊢ (𝐺 ∈ Grp → { 0 } ∈
(SubGrp‘𝐺)) |
7 | 6 | ad2antrr 762 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → { 0 } ∈
(SubGrp‘𝐺)) |
8 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐼 ↦ { 0 }) = (𝑥 ∈ 𝐼 ↦ { 0 }) |
9 | 7, 8 | fmptd 6385 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ { 0 }):𝐼⟶(SubGrp‘𝐺)) |
10 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝐺) =
(Base‘𝐺) |
11 | 10, 2 | grpidcl 17450 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
12 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 0 ∈ (Base‘𝐺)) |
13 | 12 | snssd 4340 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → { 0 } ⊆
(Base‘𝐺)) |
14 | 10, 1 | cntzsubg 17769 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ { 0 } ⊆
(Base‘𝐺)) →
((Cntz‘𝐺)‘{
0 })
∈ (SubGrp‘𝐺)) |
15 | 13, 14 | syldan 487 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → ((Cntz‘𝐺)‘{ 0 }) ∈
(SubGrp‘𝐺)) |
16 | 2 | subg0cl 17602 |
. . . . . . 7
⊢
(((Cntz‘𝐺)‘{ 0 }) ∈
(SubGrp‘𝐺) →
0 ∈
((Cntz‘𝐺)‘{
0
})) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 0 ∈ ((Cntz‘𝐺)‘{ 0 })) |
18 | 17 | snssd 4340 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → { 0 } ⊆
((Cntz‘𝐺)‘{
0
})) |
19 | 18 | adantr 481 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → { 0 } ⊆
((Cntz‘𝐺)‘{
0
})) |
20 | | simpr1 1067 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → 𝑦 ∈ 𝐼) |
21 | | eqidd 2623 |
. . . . . 6
⊢ (𝑥 = 𝑦 → { 0 } = { 0 }) |
22 | | snex 4908 |
. . . . . 6
⊢ { 0 } ∈
V |
23 | 21, 8, 22 | fvmpt3i 6287 |
. . . . 5
⊢ (𝑦 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) = { 0 }) |
24 | 20, 23 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) = { 0 }) |
25 | | simpr2 1068 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → 𝑧 ∈ 𝐼) |
26 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → { 0 } = { 0 }) |
27 | 26, 8, 22 | fvmpt3i 6287 |
. . . . . 6
⊢ (𝑧 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑧) = { 0 }) |
28 | 25, 27 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑧) = { 0 }) |
29 | 28 | fveq2d 6195 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → ((Cntz‘𝐺)‘((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑧)) = ((Cntz‘𝐺)‘{ 0 })) |
30 | 19, 24, 29 | 3sstr4d 3648 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧)) → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ⊆ ((Cntz‘𝐺)‘((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑧))) |
31 | 23 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) = { 0 }) |
32 | 31 | ineq1d 3813 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) = ({ 0 } ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦}))))) |
33 | 10 | subgacs 17629 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
34 | 33 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺))) |
35 | 34 | acsmred 16317 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
36 | | imassrn 5477 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})) ⊆ ran (𝑥 ∈ 𝐼 ↦ { 0 }) |
37 | 9 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ { 0 }):𝐼⟶(SubGrp‘𝐺)) |
38 | | frn 6053 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐼 ↦ { 0 }):𝐼⟶(SubGrp‘𝐺) → ran (𝑥 ∈ 𝐼 ↦ { 0 }) ⊆
(SubGrp‘𝐺)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ran (𝑥 ∈ 𝐼 ↦ { 0 }) ⊆
(SubGrp‘𝐺)) |
40 | | mresspw 16252 |
. . . . . . . . . . . . 13
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
41 | 35, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
42 | 39, 41 | sstrd 3613 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ran (𝑥 ∈ 𝐼 ↦ { 0 }) ⊆ 𝒫
(Base‘𝐺)) |
43 | 36, 42 | syl5ss 3614 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})) ⊆ 𝒫 (Base‘𝐺)) |
44 | | sspwuni 4611 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ ((𝑥
∈ 𝐼 ↦ { 0 }) “
(𝐼 ∖ {𝑦})) ⊆ (Base‘𝐺)) |
45 | 43, 44 | sylib 208 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})) ⊆ (Base‘𝐺)) |
46 | 3 | mrccl 16271 |
. . . . . . . . 9
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})) ⊆ (Base‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑥
∈ 𝐼 ↦ { 0 }) “
(𝐼 ∖ {𝑦}))) ∈ (SubGrp‘𝐺)) |
47 | 35, 45, 46 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑥
∈ 𝐼 ↦ { 0 }) “
(𝐼 ∖ {𝑦}))) ∈ (SubGrp‘𝐺)) |
48 | 2 | subg0cl 17602 |
. . . . . . . 8
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦}))) ∈ (SubGrp‘𝐺) → 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → 0 ∈
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) |
50 | 49 | snssd 4340 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → { 0 } ⊆
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) |
51 | | df-ss 3588 |
. . . . . 6
⊢ ({ 0 } ⊆
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦}))) ↔ ({ 0 } ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) = { 0 }) |
52 | 50, 51 | sylib 208 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ({ 0 } ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) = { 0 }) |
53 | 32, 52 | eqtrd 2656 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) = { 0 }) |
54 | | eqimss 3657 |
. . . 4
⊢ ((((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) = { 0 } → (((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) ⊆ { 0 }) |
55 | 53, 54 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ∩
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑥 ∈ 𝐼 ↦ { 0 }) “ (𝐼 ∖ {𝑦})))) ⊆ { 0 }) |
56 | 1, 2, 3, 4, 5, 9, 30, 55 | dmdprdd 18398 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝐺dom DProd (𝑥 ∈ 𝐼 ↦ { 0 })) |
57 | 8, 7 | dmmptd 6024 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → dom (𝑥 ∈ 𝐼 ↦ { 0 }) = 𝐼) |
58 | 6 | adantr 481 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → { 0 } ∈
(SubGrp‘𝐺)) |
59 | | eqimss 3657 |
. . . . 5
⊢ (((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) = { 0 } → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ⊆ { 0 }) |
60 | 31, 59 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ { 0 })‘𝑦) ⊆ { 0 }) |
61 | 56, 57, 58, 60 | dprdlub 18425 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) ⊆ { 0
}) |
62 | | dprdsubg 18423 |
. . . . 5
⊢ (𝐺dom DProd (𝑥 ∈ 𝐼 ↦ { 0 }) → (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) ∈
(SubGrp‘𝐺)) |
63 | 2 | subg0cl 17602 |
. . . . 5
⊢ ((𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) ∈
(SubGrp‘𝐺) →
0 ∈
(𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 }))) |
64 | 56, 62, 63 | 3syl 18 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 0 ∈ (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 }))) |
65 | 64 | snssd 4340 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → { 0 } ⊆ (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 }))) |
66 | 61, 65 | eqssd 3620 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) = { 0 }) |
67 | 56, 66 | jca 554 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝐺dom DProd (𝑥 ∈ 𝐼 ↦ { 0 }) ∧ (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) = { 0 })) |