Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6896 |
. . 3
โข (๐ฆ = ๐ โ (๐โ(๐โ๐ฆ)) = (๐โ(๐โ๐))) |
2 | 1 | sseq2d 4014 |
. 2
โข (๐ฆ = ๐ โ ((๐โ๐) โ (๐โ(๐โ๐ฆ)) โ (๐โ๐) โ (๐โ(๐โ๐)))) |
3 | | sneq 4638 |
. . . . 5
โข (๐ฅ = ๐ โ {๐ฅ} = {๐}) |
4 | 3 | difeq2d 4122 |
. . . 4
โข (๐ฅ = ๐ โ (๐ผ โ {๐ฅ}) = (๐ผ โ {๐})) |
5 | | fveq2 6891 |
. . . . 5
โข (๐ฅ = ๐ โ (๐โ๐ฅ) = (๐โ๐)) |
6 | 5 | sseq1d 4013 |
. . . 4
โข (๐ฅ = ๐ โ ((๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โ (๐โ๐) โ (๐โ(๐โ๐ฆ)))) |
7 | 4, 6 | raleqbidv 3342 |
. . 3
โข (๐ฅ = ๐ โ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โ โ๐ฆ โ (๐ผ โ {๐})(๐โ๐) โ (๐โ(๐โ๐ฆ)))) |
8 | | dprdcntz.1 |
. . . . . 6
โข (๐ โ ๐บdom DProd ๐) |
9 | | dprdcntz.2 |
. . . . . . . 8
โข (๐ โ dom ๐ = ๐ผ) |
10 | 8, 9 | dprddomcld 19870 |
. . . . . . 7
โข (๐ โ ๐ผ โ V) |
11 | | dprdcntz.z |
. . . . . . . 8
โข ๐ = (Cntzโ๐บ) |
12 | | eqid 2732 |
. . . . . . . 8
โข
(0gโ๐บ) = (0gโ๐บ) |
13 | | eqid 2732 |
. . . . . . . 8
โข
(mrClsโ(SubGrpโ๐บ)) = (mrClsโ(SubGrpโ๐บ)) |
14 | 11, 12, 13 | dmdprd 19867 |
. . . . . . 7
โข ((๐ผ โ V โง dom ๐ = ๐ผ) โ (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)})))) |
15 | 10, 9, 14 | syl2anc 584 |
. . . . . 6
โข (๐ โ (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)})))) |
16 | 8, 15 | mpbid 231 |
. . . . 5
โข (๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)}))) |
17 | 16 | simp3d 1144 |
. . . 4
โข (๐ โ โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)})) |
18 | | simpl 483 |
. . . . 5
โข
((โ๐ฆ โ
(๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)})
โ โ๐ฆ โ
(๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ))) |
19 | 18 | ralimi 3083 |
. . . 4
โข
(โ๐ฅ โ
๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐บ))โโช (๐
โ (๐ผ โ {๐ฅ})))) =
{(0gโ๐บ)})
โ โ๐ฅ โ
๐ผ โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ))) |
20 | 17, 19 | syl 17 |
. . 3
โข (๐ โ โ๐ฅ โ ๐ผ โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ))) |
21 | | dprdcntz.3 |
. . 3
โข (๐ โ ๐ โ ๐ผ) |
22 | 7, 20, 21 | rspcdva 3613 |
. 2
โข (๐ โ โ๐ฆ โ (๐ผ โ {๐})(๐โ๐) โ (๐โ(๐โ๐ฆ))) |
23 | | dprdcntz.4 |
. . 3
โข (๐ โ ๐ โ ๐ผ) |
24 | | dprdcntz.5 |
. . . 4
โข (๐ โ ๐ โ ๐) |
25 | 24 | necomd 2996 |
. . 3
โข (๐ โ ๐ โ ๐) |
26 | | eldifsn 4790 |
. . 3
โข (๐ โ (๐ผ โ {๐}) โ (๐ โ ๐ผ โง ๐ โ ๐)) |
27 | 23, 25, 26 | sylanbrc 583 |
. 2
โข (๐ โ ๐ โ (๐ผ โ {๐})) |
28 | 2, 22, 27 | rspcdva 3613 |
1
โข (๐ โ (๐โ๐) โ (๐โ(๐โ๐))) |