Step |
Hyp |
Ref |
Expression |
1 |
|
dprdsplit.2 |
⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) |
2 |
|
dprdsplit.i |
⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ ) |
3 |
|
dprdsplit.u |
⊢ ( 𝜑 → 𝐼 = ( 𝐶 ∪ 𝐷 ) ) |
4 |
|
dmdprdsplit.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
5 |
|
dmdprdsplit.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
6 |
|
dmdprdsplit2.1 |
⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ) |
7 |
|
dmdprdsplit2.2 |
⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) |
8 |
|
dmdprdsplit2.3 |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ) |
9 |
|
dmdprdsplit2.4 |
⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } ) |
10 |
|
eqid |
⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) |
11 |
|
dprdgrp |
⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) → 𝐺 ∈ Grp ) |
12 |
6 11
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
13 |
|
ssun1 |
⊢ 𝐶 ⊆ ( 𝐶 ∪ 𝐷 ) |
14 |
13 3
|
sseqtrrid |
⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 ) |
15 |
1 14
|
fssresd |
⊢ ( 𝜑 → ( 𝑆 ↾ 𝐶 ) : 𝐶 ⟶ ( SubGrp ‘ 𝐺 ) ) |
16 |
15
|
fdmd |
⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐶 ) = 𝐶 ) |
17 |
6 16
|
dprddomcld |
⊢ ( 𝜑 → 𝐶 ∈ V ) |
18 |
|
ssun2 |
⊢ 𝐷 ⊆ ( 𝐶 ∪ 𝐷 ) |
19 |
18 3
|
sseqtrrid |
⊢ ( 𝜑 → 𝐷 ⊆ 𝐼 ) |
20 |
1 19
|
fssresd |
⊢ ( 𝜑 → ( 𝑆 ↾ 𝐷 ) : 𝐷 ⟶ ( SubGrp ‘ 𝐺 ) ) |
21 |
20
|
fdmd |
⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐷 ) = 𝐷 ) |
22 |
7 21
|
dprddomcld |
⊢ ( 𝜑 → 𝐷 ∈ V ) |
23 |
|
unexg |
⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 ∪ 𝐷 ) ∈ V ) |
24 |
17 22 23
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 ∪ 𝐷 ) ∈ V ) |
25 |
3 24
|
eqeltrd |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
26 |
3
|
eleq2d |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↔ 𝑥 ∈ ( 𝐶 ∪ 𝐷 ) ) ) |
27 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝐶 ∪ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) |
28 |
26 27
|
bitrdi |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) ) |
29 |
1 2 3 4 5 6 7 8 9 10
|
dmdprdsplit2lem |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) ) |
30 |
|
incom |
⊢ ( 𝐶 ∩ 𝐷 ) = ( 𝐷 ∩ 𝐶 ) |
31 |
30 2
|
eqtr3id |
⊢ ( 𝜑 → ( 𝐷 ∩ 𝐶 ) = ∅ ) |
32 |
|
uncom |
⊢ ( 𝐶 ∪ 𝐷 ) = ( 𝐷 ∪ 𝐶 ) |
33 |
3 32
|
eqtrdi |
⊢ ( 𝜑 → 𝐼 = ( 𝐷 ∪ 𝐶 ) ) |
34 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
35 |
6 34
|
syl |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
36 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
37 |
7 36
|
syl |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
38 |
4 35 37 8
|
cntzrecd |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ) ) |
39 |
|
incom |
⊢ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = ( ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ) |
40 |
39 9
|
eqtr3id |
⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ) = { 0 } ) |
41 |
1 31 33 4 5 7 6 38 40 10
|
dmdprdsplit2lem |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) ) |
42 |
29 41
|
jaodan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) ) |
43 |
42
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) → ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ) |
44 |
43
|
ex |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) |
45 |
28 44
|
sylbid |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 → ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) |
46 |
45
|
3imp2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) |
47 |
28
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) |
48 |
29
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) |
49 |
41
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) |
50 |
48 49
|
jaodan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) |
51 |
47 50
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } ) |
52 |
4 5 10 12 25 1 46 51
|
dmdprdd |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |