Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
โข
(Baseโ(๐บ
โพs (๐
โ
๐))) = (Baseโ(๐บ โพs (๐ โ ๐))) |
2 | | eqid 2733 |
. 2
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
3 | | ovex 7439 |
. . 3
โข (๐ โ ๐) โ V |
4 | | eqid 2733 |
. . . 4
โข (๐บ โพs (๐ โ ๐)) = (๐บ โพs (๐ โ ๐)) |
5 | | pj1eu.a |
. . . 4
โข + =
(+gโ๐บ) |
6 | 4, 5 | ressplusg 17232 |
. . 3
โข ((๐ โ ๐) โ V โ + =
(+gโ(๐บ
โพs (๐
โ
๐)))) |
7 | 3, 6 | ax-mp 5 |
. 2
โข + =
(+gโ(๐บ
โพs (๐
โ
๐))) |
8 | | pj1eu.2 |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
9 | | pj1eu.3 |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
10 | | pj1eu.5 |
. . . 4
โข (๐ โ ๐ โ (๐โ๐)) |
11 | | pj1eu.s |
. . . . 5
โข โ =
(LSSumโ๐บ) |
12 | | pj1eu.z |
. . . . 5
โข ๐ = (Cntzโ๐บ) |
13 | 11, 12 | lsmsubg 19517 |
. . . 4
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (๐โ๐)) โ (๐ โ ๐) โ (SubGrpโ๐บ)) |
14 | 8, 9, 10, 13 | syl3anc 1372 |
. . 3
โข (๐ โ (๐ โ ๐) โ (SubGrpโ๐บ)) |
15 | 4 | subggrp 19004 |
. . 3
โข ((๐ โ ๐) โ (SubGrpโ๐บ) โ (๐บ โพs (๐ โ ๐)) โ Grp) |
16 | 14, 15 | syl 17 |
. 2
โข (๐ โ (๐บ โพs (๐ โ ๐)) โ Grp) |
17 | | subgrcl 19006 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ ๐บ โ Grp) |
18 | 8, 17 | syl 17 |
. 2
โข (๐ โ ๐บ โ Grp) |
19 | | pj1eu.o |
. . . . 5
โข 0 =
(0gโ๐บ) |
20 | | pj1eu.4 |
. . . . 5
โข (๐ โ (๐ โฉ ๐) = { 0 }) |
21 | | pj1f.p |
. . . . 5
โข ๐ = (proj1โ๐บ) |
22 | 5, 11, 19, 12, 8, 9, 20, 10, 21 | pj1f 19560 |
. . . 4
โข (๐ โ (๐๐๐):(๐ โ ๐)โถ๐) |
23 | 2 | subgss 19002 |
. . . . 5
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
24 | 8, 23 | syl 17 |
. . . 4
โข (๐ โ ๐ โ (Baseโ๐บ)) |
25 | 22, 24 | fssd 6733 |
. . 3
โข (๐ โ (๐๐๐):(๐ โ ๐)โถ(Baseโ๐บ)) |
26 | 4 | subgbas 19005 |
. . . . 5
โข ((๐ โ ๐) โ (SubGrpโ๐บ) โ (๐ โ ๐) = (Baseโ(๐บ โพs (๐ โ ๐)))) |
27 | 14, 26 | syl 17 |
. . . 4
โข (๐ โ (๐ โ ๐) = (Baseโ(๐บ โพs (๐ โ ๐)))) |
28 | 27 | feq2d 6701 |
. . 3
โข (๐ โ ((๐๐๐):(๐ โ ๐)โถ(Baseโ๐บ) โ (๐๐๐):(Baseโ(๐บ โพs (๐ โ ๐)))โถ(Baseโ๐บ))) |
29 | 25, 28 | mpbid 231 |
. 2
โข (๐ โ (๐๐๐):(Baseโ(๐บ โพs (๐ โ ๐)))โถ(Baseโ๐บ)) |
30 | 27 | eleq2d 2820 |
. . . . 5
โข (๐ โ (๐ฅ โ (๐ โ ๐) โ ๐ฅ โ (Baseโ(๐บ โพs (๐ โ ๐))))) |
31 | 27 | eleq2d 2820 |
. . . . 5
โข (๐ โ (๐ฆ โ (๐ โ ๐) โ ๐ฆ โ (Baseโ(๐บ โพs (๐ โ ๐))))) |
32 | 30, 31 | anbi12d 632 |
. . . 4
โข (๐ โ ((๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐)) โ (๐ฅ โ (Baseโ(๐บ โพs (๐ โ ๐))) โง ๐ฆ โ (Baseโ(๐บ โพs (๐ โ ๐)))))) |
33 | 32 | biimpar 479 |
. . 3
โข ((๐ โง (๐ฅ โ (Baseโ(๐บ โพs (๐ โ ๐))) โง ๐ฆ โ (Baseโ(๐บ โพs (๐ โ ๐))))) โ (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) |
34 | 5, 11, 19, 12, 8, 9, 20, 10, 21 | pj1id 19562 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ โ ๐)) โ ๐ฅ = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฅ))) |
35 | 34 | adantrr 716 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ฅ = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฅ))) |
36 | 5, 11, 19, 12, 8, 9, 20, 10, 21 | pj1id 19562 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (๐ โ ๐)) โ ๐ฆ = (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฆ))) |
37 | 36 | adantrl 715 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ฆ = (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฆ))) |
38 | 35, 37 | oveq12d 7424 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (๐ฅ + ๐ฆ) = ((((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฅ)) + (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฆ)))) |
39 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ โ (SubGrpโ๐บ)) |
40 | | grpmnd 18823 |
. . . . . . . 8
โข (๐บ โ Grp โ ๐บ โ Mnd) |
41 | 39, 17, 40 | 3syl 18 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐บ โ Mnd) |
42 | 39, 23 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ โ (Baseโ๐บ)) |
43 | | simpl 484 |
. . . . . . . . 9
โข ((๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐)) โ ๐ฅ โ (๐ โ ๐)) |
44 | | ffvelcdm 7081 |
. . . . . . . . 9
โข (((๐๐๐):(๐ โ ๐)โถ๐ โง ๐ฅ โ (๐ โ ๐)) โ ((๐๐๐)โ๐ฅ) โ ๐) |
45 | 22, 43, 44 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฅ) โ ๐) |
46 | 42, 45 | sseldd 3983 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฅ) โ (Baseโ๐บ)) |
47 | | simpr 486 |
. . . . . . . . 9
โข ((๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐)) โ ๐ฆ โ (๐ โ ๐)) |
48 | | ffvelcdm 7081 |
. . . . . . . . 9
โข (((๐๐๐):(๐ โ ๐)โถ๐ โง ๐ฆ โ (๐ โ ๐)) โ ((๐๐๐)โ๐ฆ) โ ๐) |
49 | 22, 47, 48 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฆ) โ ๐) |
50 | 42, 49 | sseldd 3983 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฆ) โ (Baseโ๐บ)) |
51 | 9 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ โ (SubGrpโ๐บ)) |
52 | 2 | subgss 19002 |
. . . . . . . . 9
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ โ (Baseโ๐บ)) |
54 | 5, 11, 19, 12, 8, 9, 20, 10, 21 | pj2f 19561 |
. . . . . . . . 9
โข (๐ โ (๐๐๐):(๐ โ ๐)โถ๐) |
55 | | ffvelcdm 7081 |
. . . . . . . . 9
โข (((๐๐๐):(๐ โ ๐)โถ๐ โง ๐ฅ โ (๐ โ ๐)) โ ((๐๐๐)โ๐ฅ) โ ๐) |
56 | 54, 43, 55 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฅ) โ ๐) |
57 | 53, 56 | sseldd 3983 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฅ) โ (Baseโ๐บ)) |
58 | | ffvelcdm 7081 |
. . . . . . . . 9
โข (((๐๐๐):(๐ โ ๐)โถ๐ โง ๐ฆ โ (๐ โ ๐)) โ ((๐๐๐)โ๐ฆ) โ ๐) |
59 | 54, 47, 58 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฆ) โ ๐) |
60 | 53, 59 | sseldd 3983 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฆ) โ (Baseโ๐บ)) |
61 | 10 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ๐ โ (๐โ๐)) |
62 | 61, 49 | sseldd 3983 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ๐ฆ) โ (๐โ๐)) |
63 | 5, 12 | cntzi 19188 |
. . . . . . . 8
โข ((((๐๐๐)โ๐ฆ) โ (๐โ๐) โง ((๐๐๐)โ๐ฅ) โ ๐) โ (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฅ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) |
64 | 62, 56, 63 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฅ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) |
65 | 2, 5, 41, 46, 50, 57, 60, 64 | mnd4g 18636 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) + (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) = ((((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฅ)) + (((๐๐๐)โ๐ฆ) + ((๐๐๐)โ๐ฆ)))) |
66 | 38, 65 | eqtr4d 2776 |
. . . . 5
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (๐ฅ + ๐ฆ) = ((((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) + (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)))) |
67 | 20 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (๐ โฉ ๐) = { 0 }) |
68 | 5 | subgcl 19011 |
. . . . . . . 8
โข (((๐ โ ๐) โ (SubGrpโ๐บ) โง ๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐)) โ (๐ฅ + ๐ฆ) โ (๐ โ ๐)) |
69 | 68 | 3expb 1121 |
. . . . . . 7
โข (((๐ โ ๐) โ (SubGrpโ๐บ) โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (๐ฅ + ๐ฆ) โ (๐ โ ๐)) |
70 | 14, 69 | sylan 581 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (๐ฅ + ๐ฆ) โ (๐ โ ๐)) |
71 | 5 | subgcl 19011 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ((๐๐๐)โ๐ฅ) โ ๐ โง ((๐๐๐)โ๐ฆ) โ ๐) โ (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โ ๐) |
72 | 39, 45, 49, 71 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โ ๐) |
73 | 5 | subgcl 19011 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ((๐๐๐)โ๐ฅ) โ ๐ โง ((๐๐๐)โ๐ฆ) โ ๐) โ (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โ ๐) |
74 | 51, 56, 59, 73 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โ ๐) |
75 | 5, 11, 19, 12, 39, 51, 67, 61, 21, 70, 72, 74 | pj1eq 19563 |
. . . . 5
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐ฅ + ๐ฆ) = ((((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) + (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) โ (((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โง ((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))))) |
76 | 66, 75 | mpbid 231 |
. . . 4
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ (((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)) โง ((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ)))) |
77 | 76 | simpld 496 |
. . 3
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ โ ๐))) โ ((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) |
78 | 33, 77 | syldan 592 |
. 2
โข ((๐ โง (๐ฅ โ (Baseโ(๐บ โพs (๐ โ ๐))) โง ๐ฆ โ (Baseโ(๐บ โพs (๐ โ ๐))))) โ ((๐๐๐)โ(๐ฅ + ๐ฆ)) = (((๐๐๐)โ๐ฅ) + ((๐๐๐)โ๐ฆ))) |
79 | 1, 2, 7, 5, 16, 18, 29, 78 | isghmd 19096 |
1
โข (๐ โ (๐๐๐) โ ((๐บ โพs (๐ โ ๐)) GrpHom ๐บ)) |