Proof of Theorem dmdprdd
Step | Hyp | Ref
| Expression |
1 | | dmdprdd.1 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
2 | | dmdprdd.3 |
. 2
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
3 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↔ (𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥)) |
4 | | necom 2835 |
. . . . . . . 8
⊢ (𝑦 ≠ 𝑥 ↔ 𝑥 ≠ 𝑦) |
5 | 4 | anbi2i 726 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥) ↔ (𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) |
6 | 3, 5 | bitri 263 |
. . . . . 6
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↔ (𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) |
7 | | dmdprdd.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
8 | 7 | 3exp2 1277 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐼 → (𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))))) |
9 | 8 | imp4b 611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) |
10 | 6, 9 | syl5bi 231 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ (𝐼 ∖ {𝑥}) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) |
11 | 10 | ralrimiv 2948 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
12 | | dmdprdd.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ { 0 }) |
13 | 2 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
14 | | dmdprd.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
15 | 14 | subg0cl 17425 |
. . . . . . . 8
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → 0 ∈ (𝑆‘𝑥)) |
16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ (𝑆‘𝑥)) |
17 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ Grp) |
18 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝐺) =
(Base‘𝐺) |
19 | 18 | subgacs 17452 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
20 | | acsmre 16136 |
. . . . . . . . . 10
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
21 | 17, 19, 20 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
22 | | imassrn 5396 |
. . . . . . . . . . . 12
⊢ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑆 |
23 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
24 | 2, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
26 | 22, 25 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (SubGrp‘𝐺)) |
27 | | mresspw 16075 |
. . . . . . . . . . . 12
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
28 | 21, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) |
29 | 26, 28 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
30 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ ((𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
31 | 29, 30 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
32 | | dmdprd.k |
. . . . . . . . . 10
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
33 | 32 | mrccl 16094 |
. . . . . . . . 9
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
34 | 21, 31, 33 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
35 | 14 | subg0cl 17425 |
. . . . . . . 8
⊢ ((𝐾‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → 0 ∈ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
37 | 16, 36 | elind 3760 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))))) |
38 | 37 | snssd 4281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → { 0 } ⊆ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))))) |
39 | 12, 38 | eqssd 3585 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 }) |
40 | 11, 39 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })) |
41 | 40 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })) |
42 | | dmdprdd.2 |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
43 | | fdm 5964 |
. . . 4
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐼) |
44 | 2, 43 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝑆 = 𝐼) |
45 | | dmdprd.z |
. . . 4
⊢ 𝑍 = (Cntz‘𝐺) |
46 | 45, 14, 32 | dmdprd 18220 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
47 | 42, 44, 46 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) |
48 | 1, 2, 41, 47 | mpbir3and 1238 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |