Step | Hyp | Ref
| Expression |
1 | | sylow1.g |
. . 3
β’ (π β πΊ β Grp) |
2 | | sylow1lem.s |
. . . 4
β’ π = {π β π« π β£ (β―βπ ) = (πβπ)} |
3 | | sylow1.x |
. . . . . 6
β’ π = (BaseβπΊ) |
4 | 3 | fvexi 6860 |
. . . . 5
β’ π β V |
5 | 4 | pwex 5339 |
. . . 4
β’ π«
π β V |
6 | 2, 5 | rabex2 5295 |
. . 3
β’ π β V |
7 | 1, 6 | jctir 522 |
. 2
β’ (π β (πΊ β Grp β§ π β V)) |
8 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
9 | | sylow1lem.a |
. . . . . . . . . . . . 13
β’ + =
(+gβπΊ) |
10 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π§ β π β¦ (π₯ + π§)) = (π§ β π β¦ (π₯ + π§)) |
11 | 3, 9, 10 | grplmulf1o 18829 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π₯ β π) β (π§ β π β¦ (π₯ + π§)):πβ1-1-ontoβπ) |
12 | 1, 8, 11 | syl2an2r 684 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π§ β π β¦ (π₯ + π§)):πβ1-1-ontoβπ) |
13 | | f1of1 6787 |
. . . . . . . . . . 11
β’ ((π§ β π β¦ (π₯ + π§)):πβ1-1-ontoβπ β (π§ β π β¦ (π₯ + π§)):πβ1-1βπ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π§ β π β¦ (π₯ + π§)):πβ1-1βπ) |
15 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
16 | | fveqeq2 6855 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β ((β―βπ ) = (πβπ) β (β―βπ¦) = (πβπ))) |
17 | 16, 2 | elrab2 3652 |
. . . . . . . . . . . . 13
β’ (π¦ β π β (π¦ β π« π β§ (β―βπ¦) = (πβπ))) |
18 | 15, 17 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π¦ β π« π β§ (β―βπ¦) = (πβπ))) |
19 | 18 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π« π) |
20 | 19 | elpwid 4573 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
21 | | f1ssres 6750 |
. . . . . . . . . 10
β’ (((π§ β π β¦ (π₯ + π§)):πβ1-1βπ β§ π¦ β π) β ((π§ β π β¦ (π₯ + π§)) βΎ π¦):π¦β1-1βπ) |
22 | 14, 20, 21 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π§ β π β¦ (π₯ + π§)) βΎ π¦):π¦β1-1βπ) |
23 | | resmpt 5995 |
. . . . . . . . . 10
β’ (π¦ β π β ((π§ β π β¦ (π₯ + π§)) βΎ π¦) = (π§ β π¦ β¦ (π₯ + π§))) |
24 | | f1eq1 6737 |
. . . . . . . . . 10
β’ (((π§ β π β¦ (π₯ + π§)) βΎ π¦) = (π§ β π¦ β¦ (π₯ + π§)) β (((π§ β π β¦ (π₯ + π§)) βΎ π¦):π¦β1-1βπ β (π§ β π¦ β¦ (π₯ + π§)):π¦β1-1βπ)) |
25 | 20, 23, 24 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (((π§ β π β¦ (π₯ + π§)) βΎ π¦):π¦β1-1βπ β (π§ β π¦ β¦ (π₯ + π§)):π¦β1-1βπ)) |
26 | 22, 25 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π§ β π¦ β¦ (π₯ + π§)):π¦β1-1βπ) |
27 | | f1f 6742 |
. . . . . . . 8
β’ ((π§ β π¦ β¦ (π₯ + π§)):π¦β1-1βπ β (π§ β π¦ β¦ (π₯ + π§)):π¦βΆπ) |
28 | | frn 6679 |
. . . . . . . 8
β’ ((π§ β π¦ β¦ (π₯ + π§)):π¦βΆπ β ran (π§ β π¦ β¦ (π₯ + π§)) β π) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ran (π§ β π¦ β¦ (π₯ + π§)) β π) |
30 | 4 | elpw2 5306 |
. . . . . . 7
β’ (ran
(π§ β π¦ β¦ (π₯ + π§)) β π« π β ran (π§ β π¦ β¦ (π₯ + π§)) β π) |
31 | 29, 30 | sylibr 233 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ran (π§ β π¦ β¦ (π₯ + π§)) β π« π) |
32 | | f1f1orn 6799 |
. . . . . . . . 9
β’ ((π§ β π¦ β¦ (π₯ + π§)):π¦β1-1βπ β (π§ β π¦ β¦ (π₯ + π§)):π¦β1-1-ontoβran
(π§ β π¦ β¦ (π₯ + π§))) |
33 | | vex 3451 |
. . . . . . . . . 10
β’ π¦ β V |
34 | 33 | f1oen 8919 |
. . . . . . . . 9
β’ ((π§ β π¦ β¦ (π₯ + π§)):π¦β1-1-ontoβran
(π§ β π¦ β¦ (π₯ + π§)) β π¦ β ran (π§ β π¦ β¦ (π₯ + π§))) |
35 | 26, 32, 34 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β ran (π§ β π¦ β¦ (π₯ + π§))) |
36 | | sylow1.f |
. . . . . . . . . 10
β’ (π β π β Fin) |
37 | | ssfi 9123 |
. . . . . . . . . 10
β’ ((π β Fin β§ π¦ β π) β π¦ β Fin) |
38 | 36, 20, 37 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β Fin) |
39 | | ssfi 9123 |
. . . . . . . . . 10
β’ ((π β Fin β§ ran (π§ β π¦ β¦ (π₯ + π§)) β π) β ran (π§ β π¦ β¦ (π₯ + π§)) β Fin) |
40 | 36, 29, 39 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ran (π§ β π¦ β¦ (π₯ + π§)) β Fin) |
41 | | hashen 14256 |
. . . . . . . . 9
β’ ((π¦ β Fin β§ ran (π§ β π¦ β¦ (π₯ + π§)) β Fin) β ((β―βπ¦) = (β―βran (π§ β π¦ β¦ (π₯ + π§))) β π¦ β ran (π§ β π¦ β¦ (π₯ + π§)))) |
42 | 38, 40, 41 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((β―βπ¦) = (β―βran (π§ β π¦ β¦ (π₯ + π§))) β π¦ β ran (π§ β π¦ β¦ (π₯ + π§)))) |
43 | 35, 42 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (β―βπ¦) = (β―βran (π§ β π¦ β¦ (π₯ + π§)))) |
44 | 18 | simprd 497 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (β―βπ¦) = (πβπ)) |
45 | 43, 44 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (β―βran (π§ β π¦ β¦ (π₯ + π§))) = (πβπ)) |
46 | | fveqeq2 6855 |
. . . . . . 7
β’ (π = ran (π§ β π¦ β¦ (π₯ + π§)) β ((β―βπ ) = (πβπ) β (β―βran (π§ β π¦ β¦ (π₯ + π§))) = (πβπ))) |
47 | 46, 2 | elrab2 3652 |
. . . . . 6
β’ (ran
(π§ β π¦ β¦ (π₯ + π§)) β π β (ran (π§ β π¦ β¦ (π₯ + π§)) β π« π β§ (β―βran (π§ β π¦ β¦ (π₯ + π§))) = (πβπ))) |
48 | 31, 45, 47 | sylanbrc 584 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ran (π§ β π¦ β¦ (π₯ + π§)) β π) |
49 | 48 | ralrimivva 3194 |
. . . 4
β’ (π β βπ₯ β π βπ¦ β π ran (π§ β π¦ β¦ (π₯ + π§)) β π) |
50 | | sylow1lem.m |
. . . . 5
β’ β =
(π₯ β π, π¦ β π β¦ ran (π§ β π¦ β¦ (π₯ + π§))) |
51 | 50 | fmpo 8004 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π ran (π§ β π¦ β¦ (π₯ + π§)) β π β β :(π Γ π)βΆπ) |
52 | 49, 51 | sylib 217 |
. . 3
β’ (π β β :(π Γ π)βΆπ) |
53 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β πΊ β Grp) |
54 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπΊ) = (0gβπΊ) |
55 | 3, 54 | grpidcl 18786 |
. . . . . . . 8
β’ (πΊ β Grp β
(0gβπΊ)
β π) |
56 | 53, 55 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π) β (0gβπΊ) β π) |
57 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β π) β π β π) |
58 | | simpr 486 |
. . . . . . . . . 10
β’ ((π₯ = (0gβπΊ) β§ π¦ = π) β π¦ = π) |
59 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ = (0gβπΊ) β§ π¦ = π) β π₯ = (0gβπΊ)) |
60 | 59 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π₯ = (0gβπΊ) β§ π¦ = π) β (π₯ + π§) = ((0gβπΊ) + π§)) |
61 | 58, 60 | mpteq12dv 5200 |
. . . . . . . . 9
β’ ((π₯ = (0gβπΊ) β§ π¦ = π) β (π§ β π¦ β¦ (π₯ + π§)) = (π§ β π β¦ ((0gβπΊ) + π§))) |
62 | 61 | rneqd 5897 |
. . . . . . . 8
β’ ((π₯ = (0gβπΊ) β§ π¦ = π) β ran (π§ β π¦ β¦ (π₯ + π§)) = ran (π§ β π β¦ ((0gβπΊ) + π§))) |
63 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
64 | 63 | mptex 7177 |
. . . . . . . . 9
β’ (π§ β π β¦ ((0gβπΊ) + π§)) β V |
65 | 64 | rnex 7853 |
. . . . . . . 8
β’ ran
(π§ β π β¦
((0gβπΊ)
+ π§)) β V |
66 | 62, 50, 65 | ovmpoa 7514 |
. . . . . . 7
β’
(((0gβπΊ) β π β§ π β π) β ((0gβπΊ) β π) = ran (π§ β π β¦ ((0gβπΊ) + π§))) |
67 | 56, 57, 66 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π) β ((0gβπΊ) β π) = ran (π§ β π β¦ ((0gβπΊ) + π§))) |
68 | 2 | ssrab3 4044 |
. . . . . . . . . . . . . 14
β’ π β π« π |
69 | 68, 57 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β π« π) |
70 | 69 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β π) |
71 | 70 | sselda 3948 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π§ β π) β π§ β π) |
72 | 3, 9, 54 | grplid 18788 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π§ β π) β ((0gβπΊ) + π§) = π§) |
73 | 53, 71, 72 | syl2an2r 684 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π§ β π) β ((0gβπΊ) + π§) = π§) |
74 | 73 | mpteq2dva 5209 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π§ β π β¦ ((0gβπΊ) + π§)) = (π§ β π β¦ π§)) |
75 | | mptresid 6008 |
. . . . . . . . 9
β’ ( I
βΎ π) = (π§ β π β¦ π§) |
76 | 74, 75 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π β§ π β π) β (π§ β π β¦ ((0gβπΊ) + π§)) = ( I βΎ π)) |
77 | 76 | rneqd 5897 |
. . . . . . 7
β’ ((π β§ π β π) β ran (π§ β π β¦ ((0gβπΊ) + π§)) = ran ( I βΎ π)) |
78 | | rnresi 6031 |
. . . . . . 7
β’ ran ( I
βΎ π) = π |
79 | 77, 78 | eqtrdi 2789 |
. . . . . 6
β’ ((π β§ π β π) β ran (π§ β π β¦ ((0gβπΊ) + π§)) = π) |
80 | 67, 79 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β π) β ((0gβπΊ) β π) = π) |
81 | | ovex 7394 |
. . . . . . . . . 10
β’ (π + π§) β V |
82 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π€ = (π + π§) β (π + π€) = (π + (π + π§))) |
83 | 81, 82 | abrexco 7195 |
. . . . . . . . 9
β’ {π’ β£ βπ€ β {π£ β£ βπ§ β π π£ = (π + π§)}π’ = (π + π€)} = {π’ β£ βπ§ β π π’ = (π + (π + π§))} |
84 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
85 | 57 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
86 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π β§ π¦ = π) β π¦ = π) |
87 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = π β§ π¦ = π) β π₯ = π) |
88 | 87 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = π β§ π¦ = π) β (π₯ + π§) = (π + π§)) |
89 | 86, 88 | mpteq12dv 5200 |
. . . . . . . . . . . . . . 15
β’ ((π₯ = π β§ π¦ = π) β (π§ β π¦ β¦ (π₯ + π§)) = (π§ β π β¦ (π + π§))) |
90 | 89 | rneqd 5897 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π β§ π¦ = π) β ran (π§ β π¦ β¦ (π₯ + π§)) = ran (π§ β π β¦ (π + π§))) |
91 | 63 | mptex 7177 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β¦ (π + π§)) β V |
92 | 91 | rnex 7853 |
. . . . . . . . . . . . . 14
β’ ran
(π§ β π β¦ (π + π§)) β V |
93 | 90, 50, 92 | ovmpoa 7514 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β (π β π) = ran (π§ β π β¦ (π + π§))) |
94 | 84, 85, 93 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (π β π) = ran (π§ β π β¦ (π + π§))) |
95 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π§ β π β¦ (π + π§)) = (π§ β π β¦ (π + π§)) |
96 | 95 | rnmpt 5914 |
. . . . . . . . . . . 12
β’ ran
(π§ β π β¦ (π + π§)) = {π£ β£ βπ§ β π π£ = (π + π§)} |
97 | 94, 96 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (π β π) = {π£ β£ βπ§ β π π£ = (π + π§)}) |
98 | 97 | rexeqdv 3313 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (βπ€ β (π β π)π’ = (π + π€) β βπ€ β {π£ β£ βπ§ β π π£ = (π + π§)}π’ = (π + π€))) |
99 | 98 | abbidv 2802 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β {π’ β£ βπ€ β (π β π)π’ = (π + π€)} = {π’ β£ βπ€ β {π£ β£ βπ§ β π π£ = (π + π§)}π’ = (π + π€)}) |
100 | 53 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β πΊ β Grp) |
101 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β π β π) |
103 | 84 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β π β π) |
104 | 71 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β π§ β π) |
105 | 3, 9 | grpass 18765 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ (π β π β§ π β π β§ π§ β π)) β ((π + π) + π§) = (π + (π + π§))) |
106 | 100, 102,
103, 104, 105 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β ((π + π) + π§) = (π + (π + π§))) |
107 | 106 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ ((((π β§ π β π) β§ (π β π β§ π β π)) β§ π§ β π) β (π’ = ((π + π) + π§) β π’ = (π + (π + π§)))) |
108 | 107 | rexbidva 3170 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (βπ§ β π π’ = ((π + π) + π§) β βπ§ β π π’ = (π + (π + π§)))) |
109 | 108 | abbidv 2802 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β {π’ β£ βπ§ β π π’ = ((π + π) + π§)} = {π’ β£ βπ§ β π π’ = (π + (π + π§))}) |
110 | 83, 99, 109 | 3eqtr4a 2799 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β {π’ β£ βπ€ β (π β π)π’ = (π + π€)} = {π’ β£ βπ§ β π π’ = ((π + π) + π§)}) |
111 | | eqid 2733 |
. . . . . . . . 9
β’ (π€ β (π β π) β¦ (π + π€)) = (π€ β (π β π) β¦ (π + π€)) |
112 | 111 | rnmpt 5914 |
. . . . . . . 8
β’ ran
(π€ β (π β π) β¦ (π + π€)) = {π’ β£ βπ€ β (π β π)π’ = (π + π€)} |
113 | | eqid 2733 |
. . . . . . . . 9
β’ (π§ β π β¦ ((π + π) + π§)) = (π§ β π β¦ ((π + π) + π§)) |
114 | 113 | rnmpt 5914 |
. . . . . . . 8
β’ ran
(π§ β π β¦ ((π + π) + π§)) = {π’ β£ βπ§ β π π’ = ((π + π) + π§)} |
115 | 110, 112,
114 | 3eqtr4g 2798 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β ran (π€ β (π β π) β¦ (π + π€)) = ran (π§ β π β¦ ((π + π) + π§))) |
116 | 52 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β β :(π Γ π)βΆπ) |
117 | 116, 84, 85 | fovcdmd 7530 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (π β π) β π) |
118 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ = π β§ π¦ = (π β π)) β π¦ = (π β π)) |
119 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ = π β§ π¦ = (π β π)) β π₯ = π) |
120 | 119 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π₯ = π β§ π¦ = (π β π)) β (π₯ + π§) = (π + π§)) |
121 | 118, 120 | mpteq12dv 5200 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ π¦ = (π β π)) β (π§ β π¦ β¦ (π₯ + π§)) = (π§ β (π β π) β¦ (π + π§))) |
122 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π§ = π€ β (π + π§) = (π + π€)) |
123 | 122 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π§ β (π β π) β¦ (π + π§)) = (π€ β (π β π) β¦ (π + π€)) |
124 | 121, 123 | eqtrdi 2789 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = (π β π)) β (π§ β π¦ β¦ (π₯ + π§)) = (π€ β (π β π) β¦ (π + π€))) |
125 | 124 | rneqd 5897 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = (π β π)) β ran (π§ β π¦ β¦ (π₯ + π§)) = ran (π€ β (π β π) β¦ (π + π€))) |
126 | | ovex 7394 |
. . . . . . . . . . 11
β’ (π β π) β V |
127 | 126 | mptex 7177 |
. . . . . . . . . 10
β’ (π€ β (π β π) β¦ (π + π€)) β V |
128 | 127 | rnex 7853 |
. . . . . . . . 9
β’ ran
(π€ β (π β π) β¦ (π + π€)) β V |
129 | 125, 50, 128 | ovmpoa 7514 |
. . . . . . . 8
β’ ((π β π β§ (π β π) β π) β (π β (π β π)) = ran (π€ β (π β π) β¦ (π + π€))) |
130 | 101, 117,
129 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (π β (π β π)) = ran (π€ β (π β π) β¦ (π + π€))) |
131 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β πΊ β Grp) |
132 | 3, 9 | grpcl 18764 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π β π β§ π β π) β (π + π) β π) |
133 | 131, 101,
84, 132 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β π) |
134 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π₯ = (π + π) β§ π¦ = π) β π¦ = π) |
135 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π₯ = (π + π) β§ π¦ = π) β π₯ = (π + π)) |
136 | 135 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((π₯ = (π + π) β§ π¦ = π) β (π₯ + π§) = ((π + π) + π§)) |
137 | 134, 136 | mpteq12dv 5200 |
. . . . . . . . . 10
β’ ((π₯ = (π + π) β§ π¦ = π) β (π§ β π¦ β¦ (π₯ + π§)) = (π§ β π β¦ ((π + π) + π§))) |
138 | 137 | rneqd 5897 |
. . . . . . . . 9
β’ ((π₯ = (π + π) β§ π¦ = π) β ran (π§ β π¦ β¦ (π₯ + π§)) = ran (π§ β π β¦ ((π + π) + π§))) |
139 | 63 | mptex 7177 |
. . . . . . . . . 10
β’ (π§ β π β¦ ((π + π) + π§)) β V |
140 | 139 | rnex 7853 |
. . . . . . . . 9
β’ ran
(π§ β π β¦ ((π + π) + π§)) β V |
141 | 138, 50, 140 | ovmpoa 7514 |
. . . . . . . 8
β’ (((π + π) β π β§ π β π) β ((π + π) β π) = ran (π§ β π β¦ ((π + π) + π§))) |
142 | 133, 85, 141 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) β π) = ran (π§ β π β¦ ((π + π) + π§))) |
143 | 115, 130,
142 | 3eqtr4rd 2784 |
. . . . . 6
β’ (((π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) β π) = (π β (π β π))) |
144 | 143 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ π β π) β βπ β π βπ β π ((π + π) β π) = (π β (π β π))) |
145 | 80, 144 | jca 513 |
. . . 4
β’ ((π β§ π β π) β (((0gβπΊ) β π) = π β§ βπ β π βπ β π ((π + π) β π) = (π β (π β π)))) |
146 | 145 | ralrimiva 3140 |
. . 3
β’ (π β βπ β π (((0gβπΊ) β π) = π β§ βπ β π βπ β π ((π + π) β π) = (π β (π β π)))) |
147 | 52, 146 | jca 513 |
. 2
β’ (π β ( β :(π Γ π)βΆπ β§ βπ β π (((0gβπΊ) β π) = π β§ βπ β π βπ β π ((π + π) β π) = (π β (π β π))))) |
148 | 3, 9, 54 | isga 19079 |
. 2
β’ ( β β
(πΊ GrpAct π) β ((πΊ β Grp β§ π β V) β§ ( β :(π Γ π)βΆπ β§ βπ β π (((0gβπΊ) β π) = π β§ βπ β π βπ β π ((π + π) β π) = (π β (π β π)))))) |
149 | 7, 147, 148 | sylanbrc 584 |
1
β’ (π β β β (πΊ GrpAct π)) |