Step | Hyp | Ref
| Expression |
1 | | sylow2b.h |
. . . 4
โข (๐ โ ๐ป โ (SubGrpโ๐บ)) |
2 | | eqid 2736 |
. . . . 5
โข (๐บ โพs ๐ป) = (๐บ โพs ๐ป) |
3 | 2 | subggrp 18799 |
. . . 4
โข (๐ป โ (SubGrpโ๐บ) โ (๐บ โพs ๐ป) โ Grp) |
4 | 1, 3 | syl 17 |
. . 3
โข (๐ โ (๐บ โพs ๐ป) โ Grp) |
5 | | sylow2b.xf |
. . . . 5
โข (๐ โ ๐ โ Fin) |
6 | | pwfi 8995 |
. . . . 5
โข (๐ โ Fin โ ๐ซ
๐ โ
Fin) |
7 | 5, 6 | sylib 217 |
. . . 4
โข (๐ โ ๐ซ ๐ โ Fin) |
8 | | sylow2b.k |
. . . . . 6
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
9 | | sylow2b.x |
. . . . . . 7
โข ๐ = (Baseโ๐บ) |
10 | | sylow2b.r |
. . . . . . 7
โข โผ =
(๐บ ~QG
๐พ) |
11 | 9, 10 | eqger 18847 |
. . . . . 6
โข (๐พ โ (SubGrpโ๐บ) โ โผ Er ๐) |
12 | 8, 11 | syl 17 |
. . . . 5
โข (๐ โ โผ Er ๐) |
13 | 12 | qsss 8594 |
. . . 4
โข (๐ โ (๐ / โผ ) โ ๐ซ
๐) |
14 | 7, 13 | ssexd 5257 |
. . 3
โข (๐ โ (๐ / โผ ) โ
V) |
15 | 4, 14 | jca 513 |
. 2
โข (๐ โ ((๐บ โพs ๐ป) โ Grp โง (๐ / โผ ) โ
V)) |
16 | | sylow2b.m |
. . . . . . 7
โข ยท =
(๐ฅ โ ๐ป, ๐ฆ โ (๐ / โผ ) โฆ ran
(๐ง โ ๐ฆ โฆ (๐ฅ + ๐ง))) |
17 | | vex 3441 |
. . . . . . . . 9
โข ๐ฆ โ V |
18 | 17 | mptex 7127 |
. . . . . . . 8
โข (๐ง โ ๐ฆ โฆ (๐ฅ + ๐ง)) โ V |
19 | 18 | rnex 7787 |
. . . . . . 7
โข ran
(๐ง โ ๐ฆ โฆ (๐ฅ + ๐ง)) โ V |
20 | 16, 19 | fnmpoi 7938 |
. . . . . 6
โข ยท Fn
(๐ป ร (๐ / โผ )) |
21 | 20 | a1i 11 |
. . . . 5
โข (๐ โ ยท Fn (๐ป ร (๐ / โผ
))) |
22 | | eqid 2736 |
. . . . . . . 8
โข (๐ / โผ ) = (๐ / โผ ) |
23 | | oveq2 7311 |
. . . . . . . . 9
โข ([๐ ] โผ = ๐ฃ โ (๐ข ยท [๐ ] โผ ) = (๐ข ยท ๐ฃ)) |
24 | 23 | eleq1d 2821 |
. . . . . . . 8
โข ([๐ ] โผ = ๐ฃ โ ((๐ข ยท [๐ ] โผ ) โ (๐ / โผ ) โ (๐ข ยท ๐ฃ) โ (๐ / โผ
))) |
25 | | sylow2b.a |
. . . . . . . . . . 11
โข + =
(+gโ๐บ) |
26 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 19266 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ (๐ข ยท [๐ ] โผ ) = [(๐ข + ๐ )] โผ ) |
27 | 10 | ovexi 7337 |
. . . . . . . . . . 11
โข โผ โ
V |
28 | | subgrcl 18801 |
. . . . . . . . . . . . . 14
โข (๐ป โ (SubGrpโ๐บ) โ ๐บ โ Grp) |
29 | 1, 28 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐บ โ Grp) |
30 | 29 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ ๐บ โ Grp) |
31 | 9 | subgss 18797 |
. . . . . . . . . . . . . . 15
โข (๐ป โ (SubGrpโ๐บ) โ ๐ป โ ๐) |
32 | 1, 31 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ป โ ๐) |
33 | 32 | sselda 3926 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ข โ ๐ป) โ ๐ข โ ๐) |
34 | 33 | 3adant3 1132 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ ๐ข โ ๐) |
35 | | simp3 1138 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ ๐ โ ๐) |
36 | 9, 25 | grpcl 18626 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง ๐ข โ ๐ โง ๐ โ ๐) โ (๐ข + ๐ ) โ ๐) |
37 | 30, 34, 35, 36 | syl3anc 1371 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ (๐ข + ๐ ) โ ๐) |
38 | | ecelqsg 8588 |
. . . . . . . . . . 11
โข (( โผ โ
V โง (๐ข + ๐ ) โ ๐) โ [(๐ข + ๐ )] โผ โ (๐ / โผ )) |
39 | 27, 37, 38 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ [(๐ข + ๐ )] โผ โ (๐ / โผ )) |
40 | 26, 39 | eqeltrd 2837 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ ๐ป โง ๐ โ ๐) โ (๐ข ยท [๐ ] โผ ) โ (๐ / โผ )) |
41 | 40 | 3expa 1118 |
. . . . . . . 8
โข (((๐ โง ๐ข โ ๐ป) โง ๐ โ ๐) โ (๐ข ยท [๐ ] โผ ) โ (๐ / โผ )) |
42 | 22, 24, 41 | ectocld 8600 |
. . . . . . 7
โข (((๐ โง ๐ข โ ๐ป) โง ๐ฃ โ (๐ / โผ )) โ (๐ข ยท ๐ฃ) โ (๐ / โผ )) |
43 | 42 | ralrimiva 3140 |
. . . . . 6
โข ((๐ โง ๐ข โ ๐ป) โ โ๐ฃ โ (๐ / โผ )(๐ข ยท ๐ฃ) โ (๐ / โผ )) |
44 | 43 | ralrimiva 3140 |
. . . . 5
โข (๐ โ โ๐ข โ ๐ป โ๐ฃ โ (๐ / โผ )(๐ข ยท ๐ฃ) โ (๐ / โผ )) |
45 | | ffnov 7429 |
. . . . 5
โข ( ยท
:(๐ป ร (๐ / โผ ))โถ(๐ / โผ ) โ ( ยท Fn
(๐ป ร (๐ / โผ )) โง
โ๐ข โ ๐ป โ๐ฃ โ (๐ / โผ )(๐ข ยท ๐ฃ) โ (๐ / โผ
))) |
46 | 21, 44, 45 | sylanbrc 584 |
. . . 4
โข (๐ โ ยท :(๐ป ร (๐ / โผ ))โถ(๐ / โผ )) |
47 | 2 | subgbas 18800 |
. . . . . . 7
โข (๐ป โ (SubGrpโ๐บ) โ ๐ป = (Baseโ(๐บ โพs ๐ป))) |
48 | 1, 47 | syl 17 |
. . . . . 6
โข (๐ โ ๐ป = (Baseโ(๐บ โพs ๐ป))) |
49 | 48 | xpeq1d 5625 |
. . . . 5
โข (๐ โ (๐ป ร (๐ / โผ )) =
((Baseโ(๐บ
โพs ๐ป))
ร (๐ / โผ
))) |
50 | 49 | feq2d 6612 |
. . . 4
โข (๐ โ ( ยท :(๐ป ร (๐ / โผ ))โถ(๐ / โผ ) โ ยท
:((Baseโ(๐บ
โพs ๐ป))
ร (๐ / โผ
))โถ(๐ / โผ
))) |
51 | 46, 50 | mpbid 232 |
. . 3
โข (๐ โ ยท
:((Baseโ(๐บ
โพs ๐ป))
ร (๐ / โผ
))โถ(๐ / โผ
)) |
52 | | oveq2 7311 |
. . . . . . 7
โข ([๐ ] โผ = ๐ข โ
((0gโ(๐บ
โพs ๐ป))
ยท
[๐ ] โผ ) =
((0gโ(๐บ
โพs ๐ป))
ยท
๐ข)) |
53 | | id 22 |
. . . . . . 7
โข ([๐ ] โผ = ๐ข โ [๐ ] โผ = ๐ข) |
54 | 52, 53 | eqeq12d 2752 |
. . . . . 6
โข ([๐ ] โผ = ๐ข โ
(((0gโ(๐บ
โพs ๐ป))
ยท
[๐ ] โผ ) = [๐ ] โผ โ
((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข)) |
55 | | oveq2 7311 |
. . . . . . . 8
โข ([๐ ] โผ = ๐ข โ ((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = ((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข)) |
56 | | oveq2 7311 |
. . . . . . . . 9
โข ([๐ ] โผ = ๐ข โ (๐ ยท [๐ ] โผ ) = (๐ ยท ๐ข)) |
57 | 56 | oveq2d 7319 |
. . . . . . . 8
โข ([๐ ] โผ = ๐ข โ (๐ ยท (๐ ยท [๐ ] โผ )) = (๐ ยท (๐ ยท ๐ข))) |
58 | 55, 57 | eqeq12d 2752 |
. . . . . . 7
โข ([๐ ] โผ = ๐ข โ (((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ )) โ ((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข)))) |
59 | 58 | 2ralbidv 3209 |
. . . . . 6
โข ([๐ ] โผ = ๐ข โ (โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ )) โ
โ๐ โ
(Baseโ(๐บ
โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข)))) |
60 | 54, 59 | anbi12d 632 |
. . . . 5
โข ([๐ ] โผ = ๐ข โ
((((0gโ(๐บ
โพs ๐ป))
ยท
[๐ ] โผ ) = [๐ ] โผ โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ ))) โ
(((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข))))) |
61 | | simpl 484 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ ๐) |
62 | 1 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ ๐ป โ (SubGrpโ๐บ)) |
63 | | eqid 2736 |
. . . . . . . . . 10
โข
(0gโ๐บ) = (0gโ๐บ) |
64 | 63 | subg0cl 18804 |
. . . . . . . . 9
โข (๐ป โ (SubGrpโ๐บ) โ
(0gโ๐บ)
โ ๐ป) |
65 | 62, 64 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (0gโ๐บ) โ ๐ป) |
66 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
67 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 19266 |
. . . . . . . 8
โข ((๐ โง (0gโ๐บ) โ ๐ป โง ๐ โ ๐) โ ((0gโ๐บ) ยท [๐ ] โผ ) =
[((0gโ๐บ)
+ ๐ )] โผ ) |
68 | 61, 65, 66, 67 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ((0gโ๐บ) ยท [๐ ] โผ ) =
[((0gโ๐บ)
+ ๐ )] โผ ) |
69 | 2, 63 | subg0 18802 |
. . . . . . . . 9
โข (๐ป โ (SubGrpโ๐บ) โ
(0gโ๐บ) =
(0gโ(๐บ
โพs ๐ป))) |
70 | 62, 69 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (0gโ๐บ) = (0gโ(๐บ โพs ๐ป))) |
71 | 70 | oveq1d 7318 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ((0gโ๐บ) ยท [๐ ] โผ ) =
((0gโ(๐บ
โพs ๐ป))
ยท
[๐ ] โผ )) |
72 | 9, 25, 63 | grplid 18650 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ โ ๐) โ ((0gโ๐บ) + ๐ ) = ๐ ) |
73 | 29, 72 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ ((0gโ๐บ) + ๐ ) = ๐ ) |
74 | 73 | eceq1d 8564 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ [((0gโ๐บ) + ๐ )] โผ = [๐ ] โผ ) |
75 | 68, 71, 74 | 3eqtr3d 2784 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ((0gโ(๐บ โพs ๐ป)) ยท [๐ ] โผ ) = [๐ ] โผ ) |
76 | 62 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ป โ (SubGrpโ๐บ)) |
77 | 76, 28 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐บ โ Grp) |
78 | 76, 31 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ป โ ๐) |
79 | | simprl 769 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ โ ๐ป) |
80 | 78, 79 | sseldd 3927 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ โ ๐) |
81 | | simprr 771 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ โ ๐ป) |
82 | 78, 81 | sseldd 3927 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ โ ๐) |
83 | 66 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐ โ ๐) |
84 | 9, 25 | grpass 18627 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ ((๐ + ๐) + ๐ ) = (๐ + (๐ + ๐ ))) |
85 | 77, 80, 82, 83, 84 | syl13anc 1372 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ((๐ + ๐) + ๐ ) = (๐ + (๐ + ๐ ))) |
86 | 85 | eceq1d 8564 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ [((๐ + ๐) + ๐ )] โผ = [(๐ + (๐ + ๐ ))] โผ ) |
87 | 61 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ๐) |
88 | 9, 25 | grpcl 18626 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ + ๐ ) โ ๐) |
89 | 77, 82, 83, 88 | syl3anc 1371 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ (๐ + ๐ ) โ ๐) |
90 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 19266 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ป โง (๐ + ๐ ) โ ๐) โ (๐ ยท [(๐ + ๐ )] โผ ) = [(๐ + (๐ + ๐ ))] โผ ) |
91 | 87, 79, 89, 90 | syl3anc 1371 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ (๐ ยท [(๐ + ๐ )] โผ ) = [(๐ + (๐ + ๐ ))] โผ ) |
92 | 86, 91 | eqtr4d 2779 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ [((๐ + ๐) + ๐ )] โผ = (๐ ยท [(๐ + ๐ )] โผ )) |
93 | 25 | subgcl 18806 |
. . . . . . . . . . 11
โข ((๐ป โ (SubGrpโ๐บ) โง ๐ โ ๐ป โง ๐ โ ๐ป) โ (๐ + ๐) โ ๐ป) |
94 | 76, 79, 81, 93 | syl3anc 1371 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ (๐ + ๐) โ ๐ป) |
95 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 19266 |
. . . . . . . . . 10
โข ((๐ โง (๐ + ๐) โ ๐ป โง ๐ โ ๐) โ ((๐ + ๐) ยท [๐ ] โผ ) = [((๐ + ๐) + ๐ )] โผ ) |
96 | 87, 94, 83, 95 | syl3anc 1371 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ((๐ + ๐) ยท [๐ ] โผ ) = [((๐ + ๐) + ๐ )] โผ ) |
97 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 19266 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ป โง ๐ โ ๐) โ (๐ ยท [๐ ] โผ ) = [(๐ + ๐ )] โผ ) |
98 | 87, 81, 83, 97 | syl3anc 1371 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ (๐ ยท [๐ ] โผ ) = [(๐ + ๐ )] โผ ) |
99 | 98 | oveq2d 7319 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ (๐ ยท (๐ ยท [๐ ] โผ )) = (๐ ยท [(๐ + ๐ )] โผ )) |
100 | 92, 96, 99 | 3eqtr4d 2786 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ป โง ๐ โ ๐ป)) โ ((๐ + ๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
))) |
101 | 100 | ralrimivva 3194 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ โ๐ โ ๐ป โ๐ โ ๐ป ((๐ + ๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
))) |
102 | 62, 47 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ ๐ป = (Baseโ(๐บ โพs ๐ป))) |
103 | 2, 25 | ressplusg 17041 |
. . . . . . . . . . . . 13
โข (๐ป โ (SubGrpโ๐บ) โ + =
(+gโ(๐บ
โพs ๐ป))) |
104 | 1, 103 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ + =
(+gโ(๐บ
โพs ๐ป))) |
105 | 104 | oveqdr 7331 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ (๐ + ๐) = (๐(+gโ(๐บ โพs ๐ป))๐)) |
106 | 105 | oveq1d 7318 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ((๐ + ๐) ยท [๐ ] โผ ) = ((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ )) |
107 | 106 | eqeq1d 2738 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (((๐ + ๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ )) โ ((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
)))) |
108 | 102, 107 | raleqbidv 3348 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (โ๐ โ ๐ป ((๐ + ๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ )) โ
โ๐ โ
(Baseโ(๐บ
โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
)))) |
109 | 102, 108 | raleqbidv 3348 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ (โ๐ โ ๐ป โ๐ โ ๐ป ((๐ + ๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ )) โ
โ๐ โ
(Baseโ(๐บ
โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
)))) |
110 | 101, 109 | mpbid 232 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
))) |
111 | 75, 110 | jca 513 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (((0gโ(๐บ โพs ๐ป)) ยท [๐ ] โผ ) = [๐ ] โผ โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท [๐ ] โผ ) = (๐ ยท (๐ ยท [๐ ] โผ
)))) |
112 | 22, 60, 111 | ectocld 8600 |
. . . 4
โข ((๐ โง ๐ข โ (๐ / โผ )) โ
(((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข)))) |
113 | 112 | ralrimiva 3140 |
. . 3
โข (๐ โ โ๐ข โ (๐ / โผ
)(((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข)))) |
114 | 51, 113 | jca 513 |
. 2
โข (๐ โ ( ยท
:((Baseโ(๐บ
โพs ๐ป))
ร (๐ / โผ
))โถ(๐ / โผ )
โง โ๐ข โ
(๐ / โผ
)(((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข))))) |
115 | | eqid 2736 |
. . 3
โข
(Baseโ(๐บ
โพs ๐ป)) =
(Baseโ(๐บ
โพs ๐ป)) |
116 | | eqid 2736 |
. . 3
โข
(+gโ(๐บ โพs ๐ป)) = (+gโ(๐บ โพs ๐ป)) |
117 | | eqid 2736 |
. . 3
โข
(0gโ(๐บ โพs ๐ป)) = (0gโ(๐บ โพs ๐ป)) |
118 | 115, 116,
117 | isga 18938 |
. 2
โข ( ยท โ
((๐บ โพs
๐ป) GrpAct (๐ / โผ )) โ (((๐บ โพs ๐ป) โ Grp โง (๐ / โผ ) โ V) โง (
ยท
:((Baseโ(๐บ
โพs ๐ป))
ร (๐ / โผ
))โถ(๐ / โผ )
โง โ๐ข โ
(๐ / โผ
)(((0gโ(๐บ
โพs ๐ป))
ยท
๐ข) = ๐ข โง โ๐ โ (Baseโ(๐บ โพs ๐ป))โ๐ โ (Baseโ(๐บ โพs ๐ป))((๐(+gโ(๐บ โพs ๐ป))๐) ยท ๐ข) = (๐ ยท (๐ ยท ๐ข)))))) |
119 | 15, 114, 118 | sylanbrc 584 |
1
โข (๐ โ ยท โ ((๐บ โพs ๐ป) GrpAct (๐ / โผ
))) |