Step | Hyp | Ref
| Expression |
1 | | dmdprdsplit.z |
. 2
⊢ 𝑍 = (Cntz‘𝐺) |
2 | | dmdprdsplit.0 |
. 2
⊢ 0 =
(0g‘𝐺) |
3 | | eqid 2610 |
. 2
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
4 | | dmdprdsplit2.1 |
. . 3
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) |
5 | | dprdgrp 18227 |
. . 3
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | dprdsplit.u |
. . 3
⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) |
8 | | dprdsplit.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
9 | | ssun1 3738 |
. . . . . . . 8
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) |
10 | 9, 7 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ⊆ 𝐼) |
11 | 8, 10 | fssresd 5984 |
. . . . . 6
⊢ (𝜑 → (𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺)) |
12 | | fdm 5964 |
. . . . . 6
⊢ ((𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐶) = 𝐶) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶) |
14 | 4, 13 | dprddomcld 18223 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ V) |
15 | | dmdprdsplit2.2 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) |
16 | | ssun2 3739 |
. . . . . . . 8
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) |
17 | 16, 7 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ 𝐼) |
18 | 8, 17 | fssresd 5984 |
. . . . . 6
⊢ (𝜑 → (𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
19 | | fdm 5964 |
. . . . . 6
⊢ ((𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺) → dom (𝑆 ↾ 𝐷) = 𝐷) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷) |
21 | 15, 20 | dprddomcld 18223 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
22 | | unexg 6857 |
. . . 4
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ∪ 𝐷) ∈ V) |
23 | 14, 21, 22 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐶 ∪ 𝐷) ∈ V) |
24 | 7, 23 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝐼 ∈ V) |
25 | 7 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ 𝑥 ∈ (𝐶 ∪ 𝐷))) |
26 | | elun 3715 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 ∪ 𝐷) ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) |
27 | 25, 26 | syl6bb 275 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↔ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷))) |
28 | | dprdsplit.i |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
29 | | dmdprdsplit2.3 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) |
30 | | dmdprdsplit2.4 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) |
31 | 8, 28, 7, 1, 2, 4, 15, 29, 30, 3 | dmdprdsplit2lem 18267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
})) |
32 | | incom 3767 |
. . . . . . . . 9
⊢ (𝐶 ∩ 𝐷) = (𝐷 ∩ 𝐶) |
33 | 32, 28 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ∩ 𝐶) = ∅) |
34 | | uncom 3719 |
. . . . . . . . 9
⊢ (𝐶 ∪ 𝐷) = (𝐷 ∪ 𝐶) |
35 | 7, 34 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 = (𝐷 ∪ 𝐶)) |
36 | | dprdsubg 18246 |
. . . . . . . . . 10
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) |
37 | 4, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) |
38 | | dprdsubg 18246 |
. . . . . . . . . 10
⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
39 | 15, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
40 | 1, 37, 39, 29 | cntzrecd 17914 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐶)))) |
41 | | incom 3767 |
. . . . . . . . 9
⊢ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = ((𝐺 DProd (𝑆 ↾ 𝐷)) ∩ (𝐺 DProd (𝑆 ↾ 𝐶))) |
42 | 41, 30 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐷)) ∩ (𝐺 DProd (𝑆 ↾ 𝐶))) = { 0 }) |
43 | 8, 33, 35, 1, 2, 15, 4, 40, 42, 3 | dmdprdsplit2lem 18267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
})) |
44 | 31, 43 | jaodan 822 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) → ((𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
})) |
45 | 44 | simpld 474 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) → (𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))))) |
46 | 45 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷) → (𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))))) |
47 | 27, 46 | sylbid 229 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 → (𝑦 ∈ 𝐼 → (𝑥 ≠ 𝑦 → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)))))) |
48 | 47 | 3imp2 1274 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) |
49 | 27 | biimpa 500 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) |
50 | 31 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
}) |
51 | 43 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
}) |
52 | 50, 51 | jaodan 822 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷)) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
}) |
53 | 49, 52 | syldan 486 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) ⊆ { 0
}) |
54 | 1, 2, 3, 6, 24, 8,
48, 53 | dmdprdd 18221 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |