Step | Hyp | Ref
| Expression |
1 | | dmdprdsplit.z |
. 2
โข ๐ = (Cntzโ๐บ) |
2 | | dmdprdsplit.0 |
. 2
โข 0 =
(0gโ๐บ) |
3 | | eqid 2732 |
. 2
โข
(mrClsโ(SubGrpโ๐บ)) = (mrClsโ(SubGrpโ๐บ)) |
4 | | dmdprdsplit2.1 |
. . 3
โข (๐ โ ๐บdom DProd (๐ โพ ๐ถ)) |
5 | | dprdgrp 19877 |
. . 3
โข (๐บdom DProd (๐ โพ ๐ถ) โ ๐บ โ Grp) |
6 | 4, 5 | syl 17 |
. 2
โข (๐ โ ๐บ โ Grp) |
7 | | dprdsplit.u |
. . 3
โข (๐ โ ๐ผ = (๐ถ โช ๐ท)) |
8 | | dprdsplit.2 |
. . . . . . 7
โข (๐ โ ๐:๐ผโถ(SubGrpโ๐บ)) |
9 | | ssun1 4172 |
. . . . . . . 8
โข ๐ถ โ (๐ถ โช ๐ท) |
10 | 9, 7 | sseqtrrid 4035 |
. . . . . . 7
โข (๐ โ ๐ถ โ ๐ผ) |
11 | 8, 10 | fssresd 6758 |
. . . . . 6
โข (๐ โ (๐ โพ ๐ถ):๐ถโถ(SubGrpโ๐บ)) |
12 | 11 | fdmd 6728 |
. . . . 5
โข (๐ โ dom (๐ โพ ๐ถ) = ๐ถ) |
13 | 4, 12 | dprddomcld 19873 |
. . . 4
โข (๐ โ ๐ถ โ V) |
14 | | dmdprdsplit2.2 |
. . . . 5
โข (๐ โ ๐บdom DProd (๐ โพ ๐ท)) |
15 | | ssun2 4173 |
. . . . . . . 8
โข ๐ท โ (๐ถ โช ๐ท) |
16 | 15, 7 | sseqtrrid 4035 |
. . . . . . 7
โข (๐ โ ๐ท โ ๐ผ) |
17 | 8, 16 | fssresd 6758 |
. . . . . 6
โข (๐ โ (๐ โพ ๐ท):๐ทโถ(SubGrpโ๐บ)) |
18 | 17 | fdmd 6728 |
. . . . 5
โข (๐ โ dom (๐ โพ ๐ท) = ๐ท) |
19 | 14, 18 | dprddomcld 19873 |
. . . 4
โข (๐ โ ๐ท โ V) |
20 | | unexg 7738 |
. . . 4
โข ((๐ถ โ V โง ๐ท โ V) โ (๐ถ โช ๐ท) โ V) |
21 | 13, 19, 20 | syl2anc 584 |
. . 3
โข (๐ โ (๐ถ โช ๐ท) โ V) |
22 | 7, 21 | eqeltrd 2833 |
. 2
โข (๐ โ ๐ผ โ V) |
23 | 7 | eleq2d 2819 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ผ โ ๐ฅ โ (๐ถ โช ๐ท))) |
24 | | elun 4148 |
. . . . 5
โข (๐ฅ โ (๐ถ โช ๐ท) โ (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท)) |
25 | 23, 24 | bitrdi 286 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ผ โ (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท))) |
26 | | dprdsplit.i |
. . . . . . . 8
โข (๐ โ (๐ถ โฉ ๐ท) = โ
) |
27 | | dmdprdsplit2.3 |
. . . . . . . 8
โข (๐ โ (๐บ DProd (๐ โพ ๐ถ)) โ (๐โ(๐บ DProd (๐ โพ ๐ท)))) |
28 | | dmdprdsplit2.4 |
. . . . . . . 8
โข (๐ โ ((๐บ DProd (๐ โพ ๐ถ)) โฉ (๐บ DProd (๐ โพ ๐ท))) = { 0 }) |
29 | 8, 26, 7, 1, 2, 4, 14, 27, 28, 3 | dmdprdsplit2lem 19917 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ถ) โ ((๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
})) |
30 | | incom 4201 |
. . . . . . . . 9
โข (๐ถ โฉ ๐ท) = (๐ท โฉ ๐ถ) |
31 | 30, 26 | eqtr3id 2786 |
. . . . . . . 8
โข (๐ โ (๐ท โฉ ๐ถ) = โ
) |
32 | | uncom 4153 |
. . . . . . . . 9
โข (๐ถ โช ๐ท) = (๐ท โช ๐ถ) |
33 | 7, 32 | eqtrdi 2788 |
. . . . . . . 8
โข (๐ โ ๐ผ = (๐ท โช ๐ถ)) |
34 | | dprdsubg 19896 |
. . . . . . . . . 10
โข (๐บdom DProd (๐ โพ ๐ถ) โ (๐บ DProd (๐ โพ ๐ถ)) โ (SubGrpโ๐บ)) |
35 | 4, 34 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐บ DProd (๐ โพ ๐ถ)) โ (SubGrpโ๐บ)) |
36 | | dprdsubg 19896 |
. . . . . . . . . 10
โข (๐บdom DProd (๐ โพ ๐ท) โ (๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ)) |
37 | 14, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐บ DProd (๐ โพ ๐ท)) โ (SubGrpโ๐บ)) |
38 | 1, 35, 37, 27 | cntzrecd 19548 |
. . . . . . . 8
โข (๐ โ (๐บ DProd (๐ โพ ๐ท)) โ (๐โ(๐บ DProd (๐ โพ ๐ถ)))) |
39 | | incom 4201 |
. . . . . . . . 9
โข ((๐บ DProd (๐ โพ ๐ถ)) โฉ (๐บ DProd (๐ โพ ๐ท))) = ((๐บ DProd (๐ โพ ๐ท)) โฉ (๐บ DProd (๐ โพ ๐ถ))) |
40 | 39, 28 | eqtr3id 2786 |
. . . . . . . 8
โข (๐ โ ((๐บ DProd (๐ โพ ๐ท)) โฉ (๐บ DProd (๐ โพ ๐ถ))) = { 0 }) |
41 | 8, 31, 33, 1, 2, 14, 4, 38, 40, 3 | dmdprdsplit2lem 19917 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ท) โ ((๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
})) |
42 | 29, 41 | jaodan 956 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท)) โ ((๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
})) |
43 | 42 | simpld 495 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท)) โ (๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ))))) |
44 | 43 | ex 413 |
. . . 4
โข (๐ โ ((๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท) โ (๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))))) |
45 | 25, 44 | sylbid 239 |
. . 3
โข (๐ โ (๐ฅ โ ๐ผ โ (๐ฆ โ ๐ผ โ (๐ฅ โ ๐ฆ โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))))) |
46 | 45 | 3imp2 1349 |
. 2
โข ((๐ โง (๐ฅ โ ๐ผ โง ๐ฆ โ ๐ผ โง ๐ฅ โ ๐ฆ)) โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ))) |
47 | 25 | biimpa 477 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ผ) โ (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท)) |
48 | 29 | simprd 496 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ถ) โ ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
}) |
49 | 41 | simprd 496 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ท) โ ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
}) |
50 | 48, 49 | jaodan 956 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ถ โจ ๐ฅ โ ๐ท)) โ ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
}) |
51 | 47, 50 | syldan 591 |
. 2
โข ((๐ โง ๐ฅ โ ๐ผ) โ ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) โ { 0
}) |
52 | 1, 2, 3, 6, 22, 8,
46, 51 | dmdprdd 19871 |
1
โข (๐ โ ๐บdom DProd ๐) |