Step | Hyp | Ref
| Expression |
1 | | simp2 1137 |
. . 3
β’ ((π β§ π΅ β π» β§ πΆ β π) β π΅ β π») |
2 | | sylow2b.r |
. . . . 5
β’ βΌ =
(πΊ ~QG
πΎ) |
3 | 2 | ovexi 7445 |
. . . 4
β’ βΌ β
V |
4 | | simp3 1138 |
. . . 4
β’ ((π β§ π΅ β π» β§ πΆ β π) β πΆ β π) |
5 | | ecelqsg 8768 |
. . . 4
β’ (( βΌ β
V β§ πΆ β π) β [πΆ] βΌ β (π / βΌ )) |
6 | 3, 4, 5 | sylancr 587 |
. . 3
β’ ((π β§ π΅ β π» β§ πΆ β π) β [πΆ] βΌ β (π / βΌ )) |
7 | | simpr 485 |
. . . . . 6
β’ ((π₯ = π΅ β§ π¦ = [πΆ] βΌ ) β π¦ = [πΆ] βΌ ) |
8 | | simpl 483 |
. . . . . . 7
β’ ((π₯ = π΅ β§ π¦ = [πΆ] βΌ ) β π₯ = π΅) |
9 | 8 | oveq1d 7426 |
. . . . . 6
β’ ((π₯ = π΅ β§ π¦ = [πΆ] βΌ ) β (π₯ + π§) = (π΅ + π§)) |
10 | 7, 9 | mpteq12dv 5239 |
. . . . 5
β’ ((π₯ = π΅ β§ π¦ = [πΆ] βΌ ) β (π§ β π¦ β¦ (π₯ + π§)) = (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
11 | 10 | rneqd 5937 |
. . . 4
β’ ((π₯ = π΅ β§ π¦ = [πΆ] βΌ ) β ran (π§ β π¦ β¦ (π₯ + π§)) = ran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
12 | | sylow2b.m |
. . . 4
β’ Β· =
(π₯ β π», π¦ β (π / βΌ ) β¦ ran
(π§ β π¦ β¦ (π₯ + π§))) |
13 | | ecexg 8709 |
. . . . . . 7
β’ ( βΌ β
V β [πΆ] βΌ β
V) |
14 | 3, 13 | ax-mp 5 |
. . . . . 6
β’ [πΆ] βΌ β
V |
15 | 14 | mptex 7227 |
. . . . 5
β’ (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β V |
16 | 15 | rnex 7905 |
. . . 4
β’ ran
(π§ β [πΆ] βΌ β¦ (π΅ + π§)) β V |
17 | 11, 12, 16 | ovmpoa 7565 |
. . 3
β’ ((π΅ β π» β§ [πΆ] βΌ β (π / βΌ )) β (π΅ Β· [πΆ] βΌ ) = ran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
18 | 1, 6, 17 | syl2anc 584 |
. 2
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π΅ Β· [πΆ] βΌ ) = ran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
19 | | sylow2b.xf |
. . . . 5
β’ (π β π β Fin) |
20 | | sylow2b.k |
. . . . . . 7
β’ (π β πΎ β (SubGrpβπΊ)) |
21 | | sylow2b.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
22 | 21, 2 | eqger 19060 |
. . . . . . 7
β’ (πΎ β (SubGrpβπΊ) β βΌ Er π) |
23 | 20, 22 | syl 17 |
. . . . . 6
β’ (π β βΌ Er π) |
24 | 23 | ecss 8751 |
. . . . 5
β’ (π β [(π΅ + πΆ)] βΌ β π) |
25 | 19, 24 | ssfid 9269 |
. . . 4
β’ (π β [(π΅ + πΆ)] βΌ β
Fin) |
26 | 25 | 3ad2ant1 1133 |
. . 3
β’ ((π β§ π΅ β π» β§ πΆ β π) β [(π΅ + πΆ)] βΌ β
Fin) |
27 | | vex 3478 |
. . . . . . . 8
β’ π§ β V |
28 | | elecg 8748 |
. . . . . . . 8
β’ ((π§ β V β§ πΆ β π) β (π§ β [πΆ] βΌ β πΆ βΌ π§)) |
29 | 27, 4, 28 | sylancr 587 |
. . . . . . 7
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β [πΆ] βΌ β πΆ βΌ π§)) |
30 | 29 | biimpa 477 |
. . . . . 6
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ π§ β [πΆ] βΌ ) β πΆ βΌ π§) |
31 | | sylow2b.h |
. . . . . . . . . . . 12
β’ (π β π» β (SubGrpβπΊ)) |
32 | | subgrcl 19013 |
. . . . . . . . . . . 12
β’ (π» β (SubGrpβπΊ) β πΊ β Grp) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΊ β Grp) |
34 | 33 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π΅ β π» β§ πΆ β π) β πΊ β Grp) |
35 | 21 | subgss 19009 |
. . . . . . . . . . . . 13
β’ (π» β (SubGrpβπΊ) β π» β π) |
36 | 31, 35 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π» β π) |
37 | 36 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β§ π΅ β π» β§ πΆ β π) β π» β π) |
38 | 37, 1 | sseldd 3983 |
. . . . . . . . . 10
β’ ((π β§ π΅ β π» β§ πΆ β π) β π΅ β π) |
39 | | sylow2b.a |
. . . . . . . . . . 11
β’ + =
(+gβπΊ) |
40 | 21, 39 | grpcl 18829 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π΅ β π β§ πΆ β π) β (π΅ + πΆ) β π) |
41 | 34, 38, 4, 40 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π΅ + πΆ) β π) |
42 | 41 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (π΅ + πΆ) β π) |
43 | 34 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β πΊ β Grp) |
44 | 38 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β π΅ β π) |
45 | 21 | subgss 19009 |
. . . . . . . . . . . . . 14
β’ (πΎ β (SubGrpβπΊ) β πΎ β π) |
46 | 20, 45 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΎ β π) |
47 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(invgβπΊ) = (invgβπΊ) |
48 | 21, 47, 39, 2 | eqgval 19059 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ πΎ β π) β (πΆ βΌ π§ β (πΆ β π β§ π§ β π β§ (((invgβπΊ)βπΆ) + π§) β πΎ))) |
49 | 33, 46, 48 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β (πΆ βΌ π§ β (πΆ β π β§ π§ β π β§ (((invgβπΊ)βπΆ) + π§) β πΎ))) |
50 | 49 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β§ π΅ β π» β§ πΆ β π) β (πΆ βΌ π§ β (πΆ β π β§ π§ β π β§ (((invgβπΊ)βπΆ) + π§) β πΎ))) |
51 | 50 | biimpa 477 |
. . . . . . . . . 10
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (πΆ β π β§ π§ β π β§ (((invgβπΊ)βπΆ) + π§) β πΎ)) |
52 | 51 | simp2d 1143 |
. . . . . . . . 9
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β π§ β π) |
53 | 21, 39 | grpcl 18829 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π΅ β π β§ π§ β π) β (π΅ + π§) β π) |
54 | 43, 44, 52, 53 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (π΅ + π§) β π) |
55 | 21, 47 | grpinvcl 18874 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ (π΅ + πΆ) β π) β ((invgβπΊ)β(π΅ + πΆ)) β π) |
56 | 34, 41, 55 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((invgβπΊ)β(π΅ + πΆ)) β π) |
57 | 56 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β ((invgβπΊ)β(π΅ + πΆ)) β π) |
58 | 21, 39 | grpass 18830 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§
(((invgβπΊ)β(π΅ + πΆ)) β π β§ π΅ β π β§ π§ β π)) β ((((invgβπΊ)β(π΅ + πΆ)) + π΅) + π§) = (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§))) |
59 | 43, 57, 44, 52, 58 | syl13anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β ((((invgβπΊ)β(π΅ + πΆ)) + π΅) + π§) = (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§))) |
60 | 21, 39, 47 | grpinvadd 18903 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β Grp β§ π΅ β π β§ πΆ β π) β ((invgβπΊ)β(π΅ + πΆ)) = (((invgβπΊ)βπΆ) +
((invgβπΊ)βπ΅))) |
61 | 34, 38, 4, 60 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((invgβπΊ)β(π΅ + πΆ)) = (((invgβπΊ)βπΆ) +
((invgβπΊ)βπ΅))) |
62 | 21, 47 | grpinvcl 18874 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ β Grp β§ πΆ β π) β ((invgβπΊ)βπΆ) β π) |
63 | 34, 4, 62 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((invgβπΊ)βπΆ) β π) |
64 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’
(-gβπΊ) = (-gβπΊ) |
65 | 21, 39, 47, 64 | grpsubval 18872 |
. . . . . . . . . . . . . . . 16
β’
((((invgβπΊ)βπΆ) β π β§ π΅ β π) β (((invgβπΊ)βπΆ)(-gβπΊ)π΅) = (((invgβπΊ)βπΆ) +
((invgβπΊ)βπ΅))) |
66 | 63, 38, 65 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π΅ β π» β§ πΆ β π) β (((invgβπΊ)βπΆ)(-gβπΊ)π΅) = (((invgβπΊ)βπΆ) +
((invgβπΊ)βπ΅))) |
67 | 61, 66 | eqtr4d 2775 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((invgβπΊ)β(π΅ + πΆ)) = (((invgβπΊ)βπΆ)(-gβπΊ)π΅)) |
68 | 67 | oveq1d 7426 |
. . . . . . . . . . . . 13
β’ ((π β§ π΅ β π» β§ πΆ β π) β (((invgβπΊ)β(π΅ + πΆ)) + π΅) = ((((invgβπΊ)βπΆ)(-gβπΊ)π΅) + π΅)) |
69 | 21, 39, 64 | grpnpcan 18917 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§
((invgβπΊ)βπΆ) β π β§ π΅ β π) β ((((invgβπΊ)βπΆ)(-gβπΊ)π΅) + π΅) = ((invgβπΊ)βπΆ)) |
70 | 34, 63, 38, 69 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((((invgβπΊ)βπΆ)(-gβπΊ)π΅) + π΅) = ((invgβπΊ)βπΆ)) |
71 | 68, 70 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ ((π β§ π΅ β π» β§ πΆ β π) β (((invgβπΊ)β(π΅ + πΆ)) + π΅) = ((invgβπΊ)βπΆ)) |
72 | 71 | oveq1d 7426 |
. . . . . . . . . . 11
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((((invgβπΊ)β(π΅ + πΆ)) + π΅) + π§) = (((invgβπΊ)βπΆ) + π§)) |
73 | 72 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β ((((invgβπΊ)β(π΅ + πΆ)) + π΅) + π§) = (((invgβπΊ)βπΆ) + π§)) |
74 | 59, 73 | eqtr3d 2774 |
. . . . . . . . 9
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) = (((invgβπΊ)βπΆ) + π§)) |
75 | 51 | simp3d 1144 |
. . . . . . . . 9
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (((invgβπΊ)βπΆ) + π§) β πΎ) |
76 | 74, 75 | eqeltrd 2833 |
. . . . . . . 8
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) β πΎ) |
77 | 21, 47, 39, 2 | eqgval 19059 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ πΎ β π) β ((π΅ + πΆ) βΌ (π΅ + π§) β ((π΅ + πΆ) β π β§ (π΅ + π§) β π β§ (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) β πΎ))) |
78 | 33, 46, 77 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β ((π΅ + πΆ) βΌ (π΅ + π§) β ((π΅ + πΆ) β π β§ (π΅ + π§) β π β§ (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) β πΎ))) |
79 | 78 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((π΅ + πΆ) βΌ (π΅ + π§) β ((π΅ + πΆ) β π β§ (π΅ + π§) β π β§ (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) β πΎ))) |
80 | 79 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β ((π΅ + πΆ) βΌ (π΅ + π§) β ((π΅ + πΆ) β π β§ (π΅ + π§) β π β§ (((invgβπΊ)β(π΅ + πΆ)) + (π΅ + π§)) β πΎ))) |
81 | 42, 54, 76, 80 | mpbir3and 1342 |
. . . . . . 7
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (π΅ + πΆ) βΌ (π΅ + π§)) |
82 | | ovex 7444 |
. . . . . . . 8
β’ (π΅ + π§) β V |
83 | | ovex 7444 |
. . . . . . . 8
β’ (π΅ + πΆ) β V |
84 | 82, 83 | elec 8749 |
. . . . . . 7
β’ ((π΅ + π§) β [(π΅ + πΆ)] βΌ β (π΅ + πΆ) βΌ (π΅ + π§)) |
85 | 81, 84 | sylibr 233 |
. . . . . 6
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ πΆ βΌ π§) β (π΅ + π§) β [(π΅ + πΆ)] βΌ ) |
86 | 30, 85 | syldan 591 |
. . . . 5
β’ (((π β§ π΅ β π» β§ πΆ β π) β§ π§ β [πΆ] βΌ ) β (π΅ + π§) β [(π΅ + πΆ)] βΌ ) |
87 | 86 | fmpttd 7116 |
. . . 4
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ βΆ[(π΅ + πΆ)] βΌ ) |
88 | 87 | frnd 6725 |
. . 3
β’ ((π β§ π΅ β π» β§ πΆ β π) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [(π΅ + πΆ)] βΌ ) |
89 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π§ β π β¦ (π΅ + π§)) = (π§ β π β¦ (π΅ + π§)) |
90 | 21, 39, 89 | grplmulf1o 18899 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π΅ β π) β (π§ β π β¦ (π΅ + π§)):πβ1-1-ontoβπ) |
91 | 34, 38, 90 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β π β¦ (π΅ + π§)):πβ1-1-ontoβπ) |
92 | | f1of1 6832 |
. . . . . . . . 9
β’ ((π§ β π β¦ (π΅ + π§)):πβ1-1-ontoβπ β (π§ β π β¦ (π΅ + π§)):πβ1-1βπ) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β π β¦ (π΅ + π§)):πβ1-1βπ) |
94 | 23 | ecss 8751 |
. . . . . . . . 9
β’ (π β [πΆ] βΌ β π) |
95 | 94 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π΅ β π» β§ πΆ β π) β [πΆ] βΌ β π) |
96 | | f1ssres 6795 |
. . . . . . . 8
β’ (((π§ β π β¦ (π΅ + π§)):πβ1-1βπ β§ [πΆ] βΌ β π) β ((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ):[πΆ] βΌ β1-1βπ) |
97 | 93, 95, 96 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π΅ β π» β§ πΆ β π) β ((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ):[πΆ] βΌ β1-1βπ) |
98 | | resmpt 6037 |
. . . . . . . 8
β’ ([πΆ] βΌ β π β ((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ) = (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
99 | | f1eq1 6782 |
. . . . . . . 8
β’ (((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ) = (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β (((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ):[πΆ] βΌ β1-1βπ β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1βπ)) |
100 | 95, 98, 99 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π΅ β π» β§ πΆ β π) β (((π§ β π β¦ (π΅ + π§)) βΎ [πΆ] βΌ ):[πΆ] βΌ β1-1βπ β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1βπ)) |
101 | 97, 100 | mpbid 231 |
. . . . . 6
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1βπ) |
102 | | f1f1orn 6844 |
. . . . . 6
β’ ((π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1βπ β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1-ontoβran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
103 | 101, 102 | syl 17 |
. . . . 5
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1-ontoβran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
104 | 14 | f1oen 8971 |
. . . . 5
β’ ((π§ β [πΆ] βΌ β¦ (π΅ + π§)):[πΆ] βΌ β1-1-ontoβran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [πΆ] βΌ β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§))) |
105 | | ensym 9001 |
. . . . 5
β’ ([πΆ] βΌ β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [πΆ] βΌ ) |
106 | 103, 104,
105 | 3syl 18 |
. . . 4
β’ ((π β§ π΅ β π» β§ πΆ β π) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [πΆ] βΌ ) |
107 | 20 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π β§ π΅ β π» β§ πΆ β π) β πΎ β (SubGrpβπΊ)) |
108 | 21, 2 | eqgen 19063 |
. . . . . . 7
β’ ((πΎ β (SubGrpβπΊ) β§ [πΆ] βΌ β (π / βΌ )) β πΎ β [πΆ] βΌ ) |
109 | 107, 6, 108 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π΅ β π» β§ πΆ β π) β πΎ β [πΆ] βΌ ) |
110 | | ensym 9001 |
. . . . . 6
β’ (πΎ β [πΆ] βΌ β [πΆ] βΌ β πΎ) |
111 | 109, 110 | syl 17 |
. . . . 5
β’ ((π β§ π΅ β π» β§ πΆ β π) β [πΆ] βΌ β πΎ) |
112 | | ecelqsg 8768 |
. . . . . . 7
β’ (( βΌ β
V β§ (π΅ + πΆ) β π) β [(π΅ + πΆ)] βΌ β (π / βΌ )) |
113 | 3, 41, 112 | sylancr 587 |
. . . . . 6
β’ ((π β§ π΅ β π» β§ πΆ β π) β [(π΅ + πΆ)] βΌ β (π / βΌ )) |
114 | 21, 2 | eqgen 19063 |
. . . . . 6
β’ ((πΎ β (SubGrpβπΊ) β§ [(π΅ + πΆ)] βΌ β (π / βΌ )) β πΎ β [(π΅ + πΆ)] βΌ ) |
115 | 107, 113,
114 | syl2anc 584 |
. . . . 5
β’ ((π β§ π΅ β π» β§ πΆ β π) β πΎ β [(π΅ + πΆ)] βΌ ) |
116 | | entr 9004 |
. . . . 5
β’ (([πΆ] βΌ β πΎ β§ πΎ β [(π΅ + πΆ)] βΌ ) β [πΆ] βΌ β [(π΅ + πΆ)] βΌ ) |
117 | 111, 115,
116 | syl2anc 584 |
. . . 4
β’ ((π β§ π΅ β π» β§ πΆ β π) β [πΆ] βΌ β [(π΅ + πΆ)] βΌ ) |
118 | | entr 9004 |
. . . 4
β’ ((ran
(π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [πΆ] βΌ β§ [πΆ] βΌ β [(π΅ + πΆ)] βΌ ) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [(π΅ + πΆ)] βΌ ) |
119 | 106, 117,
118 | syl2anc 584 |
. . 3
β’ ((π β§ π΅ β π» β§ πΆ β π) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [(π΅ + πΆ)] βΌ ) |
120 | | fisseneq 9259 |
. . 3
β’ (([(π΅ + πΆ)] βΌ β Fin β§
ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [(π΅ + πΆ)] βΌ β§ ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) β [(π΅ + πΆ)] βΌ ) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) = [(π΅ + πΆ)] βΌ ) |
121 | 26, 88, 119, 120 | syl3anc 1371 |
. 2
β’ ((π β§ π΅ β π» β§ πΆ β π) β ran (π§ β [πΆ] βΌ β¦ (π΅ + π§)) = [(π΅ + πΆ)] βΌ ) |
122 | 18, 121 | eqtrd 2772 |
1
β’ ((π β§ π΅ β π» β§ πΆ β π) β (π΅ Β· [πΆ] βΌ ) = [(π΅ + πΆ)] βΌ ) |