Step | Hyp | Ref
| Expression |
1 | | elex 3492 |
. . . . 5
โข (๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))} โ ๐ โ V) |
2 | 1 | a1i 11 |
. . . 4
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ (๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))} โ ๐ โ V)) |
3 | | fex 7227 |
. . . . . . 7
โข ((๐:๐ผโถ(SubGrpโ๐บ) โง ๐ผ โ ๐) โ ๐ โ V) |
4 | 3 | expcom 414 |
. . . . . 6
โข (๐ผ โ ๐ โ (๐:๐ผโถ(SubGrpโ๐บ) โ ๐ โ V)) |
5 | 4 | adantr 481 |
. . . . 5
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ (๐:๐ผโถ(SubGrpโ๐บ) โ ๐ โ V)) |
6 | 5 | adantrd 492 |
. . . 4
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ ((๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })) โ ๐ โ V)) |
7 | | df-sbc 3778 |
. . . . . 6
โข
([๐ / โ](โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })) โ ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))}) |
8 | | simpr 485 |
. . . . . . 7
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง ๐ โ V) โ ๐ โ V) |
9 | | simpr 485 |
. . . . . . . . . 10
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ โ = ๐) |
10 | 9 | dmeqd 5905 |
. . . . . . . . . . 11
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ dom โ = dom ๐) |
11 | | simplr 767 |
. . . . . . . . . . 11
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ dom ๐ = ๐ผ) |
12 | 10, 11 | eqtrd 2772 |
. . . . . . . . . 10
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ dom โ = ๐ผ) |
13 | 9, 12 | feq12d 6705 |
. . . . . . . . 9
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โ:dom โโถ(SubGrpโ๐บ) โ ๐:๐ผโถ(SubGrpโ๐บ))) |
14 | 12 | difeq1d 4121 |
. . . . . . . . . . . 12
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (dom โ โ {๐ฅ}) = (๐ผ โ {๐ฅ})) |
15 | 9 | fveq1d 6893 |
. . . . . . . . . . . . 13
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โโ๐ฅ) = (๐โ๐ฅ)) |
16 | 9 | fveq1d 6893 |
. . . . . . . . . . . . . 14
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โโ๐ฆ) = (๐โ๐ฆ)) |
17 | 16 | fveq2d 6895 |
. . . . . . . . . . . . 13
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (๐โ(โโ๐ฆ)) = (๐โ(๐โ๐ฆ))) |
18 | 15, 17 | sseq12d 4015 |
. . . . . . . . . . . 12
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ ((โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โ (๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))) |
19 | 14, 18 | raleqbidv 3342 |
. . . . . . . . . . 11
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โ โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)))) |
20 | 9, 14 | imaeq12d 6060 |
. . . . . . . . . . . . . . 15
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โ โ (dom โ โ {๐ฅ})) = (๐ โ (๐ผ โ {๐ฅ}))) |
21 | 20 | unieqd 4922 |
. . . . . . . . . . . . . 14
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ โช (โ โ (dom โ โ {๐ฅ})) = โช (๐ โ (๐ผ โ {๐ฅ}))) |
22 | 21 | fveq2d 6895 |
. . . . . . . . . . . . 13
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (๐พโโช (โ โ (dom โ โ {๐ฅ}))) = (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) |
23 | 15, 22 | ineq12d 4213 |
. . . . . . . . . . . 12
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ}))))) |
24 | 23 | eqeq1d 2734 |
. . . . . . . . . . 11
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 } โ ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })) |
25 | 19, 24 | anbi12d 631 |
. . . . . . . . . 10
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ ((โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }) โ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }))) |
26 | 12, 25 | raleqbidv 3342 |
. . . . . . . . 9
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ (โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }) โ โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }))) |
27 | 13, 26 | anbi12d 631 |
. . . . . . . 8
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง โ = ๐) โ ((โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })) โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
28 | 27 | adantlr 713 |
. . . . . . 7
โข ((((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง ๐ โ V) โง โ = ๐) โ ((โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })) โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
29 | 8, 28 | sbcied 3822 |
. . . . . 6
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง ๐ โ V) โ ([๐ / โ](โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })) โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
30 | 7, 29 | bitr3id 284 |
. . . . 5
โข (((๐ผ โ ๐ โง dom ๐ = ๐ผ) โง ๐ โ V) โ (๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))} โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
31 | 30 | ex 413 |
. . . 4
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ (๐ โ V โ (๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))} โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }))))) |
32 | 2, 6, 31 | pm5.21ndd 380 |
. . 3
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ (๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))} โ (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
33 | 32 | anbi2d 629 |
. 2
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ ((๐บ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))}) โ (๐บ โ Grp โง (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 }))))) |
34 | | df-br 5149 |
. . 3
โข (๐บdom DProd ๐ โ โจ๐บ, ๐โฉ โ dom DProd ) |
35 | | fvex 6904 |
. . . . . . . . . . 11
โข (๐ โ๐ฅ) โ V |
36 | 35 | rgenw 3065 |
. . . . . . . . . 10
โข
โ๐ฅ โ dom
๐ (๐ โ๐ฅ) โ V |
37 | | ixpexg 8915 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
dom ๐ (๐ โ๐ฅ) โ V โ X๐ฅ โ
dom ๐ (๐ โ๐ฅ) โ V) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
โข X๐ฅ โ
dom ๐ (๐ โ๐ฅ) โ V |
39 | 38 | mptrabex 7226 |
. . . . . . . 8
โข (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
40 | 39 | rnex 7902 |
. . . . . . 7
โข ran
(๐ โ {โ โ X๐ฅ โ
dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
41 | 40 | rgen2w 3066 |
. . . . . 6
โข
โ๐ โ Grp
โ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))}ran (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
42 | | df-dprd 19864 |
. . . . . . 7
โข DProd =
(๐ โ Grp, ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))} โฆ ran (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
43 | 42 | fmpox 8052 |
. . . . . 6
โข
(โ๐ โ
Grp โ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))}ran (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V โ DProd
:โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))})โถV) |
44 | 41, 43 | mpbi 229 |
. . . . 5
โข DProd
:โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))})โถV |
45 | 44 | fdmi 6729 |
. . . 4
โข dom DProd
= โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))}) |
46 | 45 | eleq2i 2825 |
. . 3
โข
(โจ๐บ, ๐โฉ โ dom DProd โ
โจ๐บ, ๐โฉ โ โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))})) |
47 | | fveq2 6891 |
. . . . . . 7
โข (๐ = ๐บ โ (SubGrpโ๐) = (SubGrpโ๐บ)) |
48 | 47 | feq3d 6704 |
. . . . . 6
โข (๐ = ๐บ โ (โ:dom โโถ(SubGrpโ๐) โ โ:dom โโถ(SubGrpโ๐บ))) |
49 | | fveq2 6891 |
. . . . . . . . . . . 12
โข (๐ = ๐บ โ (Cntzโ๐) = (Cntzโ๐บ)) |
50 | | dmdprd.z |
. . . . . . . . . . . 12
โข ๐ = (Cntzโ๐บ) |
51 | 49, 50 | eqtr4di 2790 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ (Cntzโ๐) = ๐) |
52 | 51 | fveq1d 6893 |
. . . . . . . . . 10
โข (๐ = ๐บ โ ((Cntzโ๐)โ(โโ๐ฆ)) = (๐โ(โโ๐ฆ))) |
53 | 52 | sseq2d 4014 |
. . . . . . . . 9
โข (๐ = ๐บ โ ((โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โ (โโ๐ฅ) โ (๐โ(โโ๐ฆ)))) |
54 | 53 | ralbidv 3177 |
. . . . . . . 8
โข (๐ = ๐บ โ (โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โ โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)))) |
55 | 47 | fveq2d 6895 |
. . . . . . . . . . . 12
โข (๐ = ๐บ โ (mrClsโ(SubGrpโ๐)) =
(mrClsโ(SubGrpโ๐บ))) |
56 | | dmdprd.k |
. . . . . . . . . . . 12
โข ๐พ =
(mrClsโ(SubGrpโ๐บ)) |
57 | 55, 56 | eqtr4di 2790 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ (mrClsโ(SubGrpโ๐)) = ๐พ) |
58 | 57 | fveq1d 6893 |
. . . . . . . . . 10
โข (๐ = ๐บ โ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ}))) = (๐พโโช (โ โ (dom โ โ {๐ฅ})))) |
59 | 58 | ineq2d 4212 |
. . . . . . . . 9
โข (๐ = ๐บ โ ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) = ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ}))))) |
60 | | fveq2 6891 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ (0gโ๐) = (0gโ๐บ)) |
61 | | dmdprd.0 |
. . . . . . . . . . 11
โข 0 =
(0gโ๐บ) |
62 | 60, 61 | eqtr4di 2790 |
. . . . . . . . . 10
โข (๐ = ๐บ โ (0gโ๐) = 0 ) |
63 | 62 | sneqd 4640 |
. . . . . . . . 9
โข (๐ = ๐บ โ {(0gโ๐)} = { 0 }) |
64 | 59, 63 | eqeq12d 2748 |
. . . . . . . 8
โข (๐ = ๐บ โ (((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}
โ ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })) |
65 | 54, 64 | anbi12d 631 |
. . . . . . 7
โข (๐ = ๐บ โ ((โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)})
โ (โ๐ฆ โ
(dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))) |
66 | 65 | ralbidv 3177 |
. . . . . 6
โข (๐ = ๐บ โ (โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)})
โ โ๐ฅ โ dom
โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))) |
67 | 48, 66 | anbi12d 631 |
. . . . 5
โข (๐ = ๐บ โ ((โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))
โ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 })))) |
68 | 67 | abbidv 2801 |
. . . 4
โข (๐ = ๐บ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))} = {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))}) |
69 | 68 | opeliunxp2 5838 |
. . 3
โข
(โจ๐บ, ๐โฉ โ โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))}) โ (๐บ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))})) |
70 | 34, 46, 69 | 3bitri 296 |
. 2
โข (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐บ) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ (๐โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ (๐พโโช (โ โ (dom โ โ {๐ฅ})))) = { 0 }))})) |
71 | | 3anass 1095 |
. 2
โข ((๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })) โ (๐บ โ Grp โง (๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |
72 | 33, 70, 71 | 3bitr4g 313 |
1
โข ((๐ผ โ ๐ โง dom ๐ = ๐ผ) โ (๐บdom DProd ๐ โ (๐บ โ Grp โง ๐:๐ผโถ(SubGrpโ๐บ) โง โ๐ฅ โ ๐ผ (โ๐ฆ โ (๐ผ โ {๐ฅ})(๐โ๐ฅ) โ (๐โ(๐โ๐ฆ)) โง ((๐โ๐ฅ) โฉ (๐พโโช (๐ โ (๐ผ โ {๐ฅ})))) = { 0 })))) |