Proof of Theorem dmdprdd
Step | Hyp | Ref
| Expression |
1 | | dmdprdd.1 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
2 | | dmdprdd.3 |
. 2
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
3 | | eldifsn 4700 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↔ (𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥)) |
4 | | necom 2994 |
. . . . . . . 8
⊢ (𝑦 ≠ 𝑥 ↔ 𝑥 ≠ 𝑦) |
5 | 4 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥) ↔ (𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) |
6 | 3, 5 | bitri 278 |
. . . . . 6
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↔ (𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) |
7 | | dmdprdd.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
8 | 7 | 3exp2 1356 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐼 → (𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))))) |
9 | 8 | imp4b 425 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) |
10 | 6, 9 | syl5bi 245 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ (𝐼 ∖ {𝑥}) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) |
11 | 10 | ralrimiv 3104 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
12 | | dmdprdd.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ { 0 }) |
13 | 2 | ffvelrnda 6904 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
14 | | dmdprd.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
15 | 14 | subg0cl 18551 |
. . . . . . . 8
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → 0 ∈ (𝑆‘𝑥)) |
16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ (𝑆‘𝑥)) |
17 | 1 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Grp) |
18 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐺) =
(Base‘𝐺) |
19 | 18 | subgacs 18577 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
20 | | acsmre 17155 |
. . . . . . . . . 10
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
21 | 17, 19, 20 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
22 | | imassrn 5940 |
. . . . . . . . . . . 12
⊢ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑆 |
23 | 2 | frnd 6553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
25 | 22, 24 | sstrid 3912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (SubGrp‘𝐺)) |
26 | | mresspw 17095 |
. . . . . . . . . . . 12
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
27 | 21, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
28 | 25, 27 | sstrd 3911 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
29 | | sspwuni 5008 |
. . . . . . . . . 10
⊢ ((𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
30 | 28, 29 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
31 | | dmdprd.k |
. . . . . . . . . 10
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
32 | 31 | mrccl 17114 |
. . . . . . . . 9
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
33 | 21, 30, 32 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
34 | 14 | subg0cl 18551 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → 0 ∈ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
36 | 16, 35 | elind 4108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))))) |
37 | 36 | snssd 4722 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → { 0 } ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))))) |
38 | 12, 37 | eqssd 3918 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) |
39 | 11, 38 | jca 515 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })) |
40 | 39 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })) |
41 | | dmdprdd.2 |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
42 | 2 | fdmd 6556 |
. . 3
⊢ (𝜑 → dom 𝑆 = 𝐼) |
43 | | dmdprd.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝐺) |
44 | 43, 14, 31 | dmdprd 19385 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
45 | 41, 42, 44 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
46 | 1, 2, 40, 45 | mpbir3and 1344 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |