Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . 4
โข (๐ฅ = ๐ โ (๐โ๐ฅ) = (๐โ๐)) |
2 | | sneq 4638 |
. . . . . . . 8
โข (๐ฅ = ๐ โ {๐ฅ} = {๐}) |
3 | 2 | difeq2d 4122 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ผ โ {๐ฅ}) = (๐ผ โ {๐})) |
4 | 3 | imaeq2d 6059 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ โ (๐ผ โ {๐ฅ})) = (๐ โ (๐ผ โ {๐}))) |
5 | 4 | unieqd 4922 |
. . . . 5
โข (๐ฅ = ๐ โ โช (๐ โ (๐ผ โ {๐ฅ})) = โช (๐ โ (๐ผ โ {๐}))) |
6 | 5 | fveq2d 6895 |
. . . 4
โข (๐ฅ = ๐ โ (๐พโโช (๐ โ (๐ผ โ {๐ฅ}))) = (๐พโโช (๐ โ (๐ผ โ {๐})))) |
7 | 1, 6 | ineq12d 4213 |
. . 3
โข (๐ฅ = ๐ โ ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = ((๐โ๐) โฉ (๐พโโช (๐ โ (๐ผ โ {๐}))))) |
8 | 7 | eqeq1d 2733 |
. 2
โข (๐ฅ = ๐ โ (((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 } โ ((๐โ๐) โฉ (๐พโโช (๐ โ (๐ผ โ {๐})))) = { 0 })) |
9 | | dprdcntz.1 |
. . . . 5
โข (๐ โ ๐บdom DProd ๐) |
10 | | dprdcntz.2 |
. . . . . . 7
โข (๐ โ dom ๐ = ๐ผ) |
11 | 9, 10 | dprddomcld 19913 |
. . . . . 6
โข (๐ โ ๐ผ โ V) |
12 | | eqid 2731 |
. . . . . . 7
โข
(Cntzโ๐บ) =
(Cntzโ๐บ) |
13 | | dprddisj.0 |
. . . . . . 7
โข 0 =
(0gโ๐บ) |
14 | | dprddisj.k |
. . . . . . 7
โข ๐พ =
(mrClsโ(SubGrpโ๐บ)) |
15 | 12, 13, 14 | dmdprd 19910 |
. . . . . 6
โข ((๐ผ โ V โง dom ๐ = ๐ผ) โ (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
16 | 11, 10, 15 | syl2anc 583 |
. . . . 5
โข (๐ โ (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
17 | 9, 16 | mpbid 231 |
. . . 4
โข (๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }))) |
18 | 17 | simp3d 1143 |
. . 3
โข (๐ โ โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })) |
19 | | simpr 484 |
. . . 4
โข
((โ๐ฆ โ
(๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }) โ ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }) |
20 | 19 | ralimi 3082 |
. . 3
โข
(โ๐ฅ โ
๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ ((Cntzโ๐บ)โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }) โ โ๐ฅ โ ๐ผ ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }) |
21 | 18, 20 | syl 17 |
. 2
โข (๐ โ โ๐ฅ โ ๐ผ ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }) |
22 | | dprdcntz.3 |
. 2
โข (๐ โ ๐ โ ๐ผ) |
23 | 8, 21, 22 | rspcdva 3613 |
1
โข (๐ โ ((๐โ๐) โฉ (๐พโโช (๐ โ (๐ผ โ {๐})))) = { 0 }) |