Step | Hyp | Ref
| Expression |
1 | | cycsubg.x |
. . . . . . . 8
โข ๐ = (Baseโ๐บ) |
2 | | cycsubg.t |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
3 | 1, 2 | mulgcl 18894 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ฅ โ โค โง ๐ด โ ๐) โ (๐ฅ ยท ๐ด) โ ๐) |
4 | 3 | 3expa 1119 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ฅ โ โค) โง ๐ด โ ๐) โ (๐ฅ ยท ๐ด) โ ๐) |
5 | 4 | an32s 651 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฅ โ โค) โ (๐ฅ ยท ๐ด) โ ๐) |
6 | | cycsubg.f |
. . . . 5
โข ๐น = (๐ฅ โ โค โฆ (๐ฅ ยท ๐ด)) |
7 | 5, 6 | fmptd 7063 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐น:โคโถ๐) |
8 | 7 | frnd 6677 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ran ๐น โ ๐) |
9 | 7 | ffnd 6670 |
. . . . 5
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐น Fn โค) |
10 | | 1z 12534 |
. . . . 5
โข 1 โ
โค |
11 | | fnfvelrn 7032 |
. . . . 5
โข ((๐น Fn โค โง 1 โ
โค) โ (๐นโ1)
โ ran ๐น) |
12 | 9, 10, 11 | sylancl 587 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐นโ1) โ ran ๐น) |
13 | 12 | ne0d 4296 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ran ๐น โ โ
) |
14 | | df-3an 1090 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค โง ๐ด โ ๐) โ ((๐ โ โค โง ๐ โ โค) โง ๐ด โ ๐)) |
15 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข
(+gโ๐บ) = (+gโ๐บ) |
16 | 1, 2, 15 | mulgdir 18909 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ด โ ๐)) โ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(๐ ยท ๐ด))) |
17 | 14, 16 | sylan2br 596 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง ((๐ โ โค โง ๐ โ โค) โง ๐ด โ ๐)) โ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(๐ ยท ๐ด))) |
18 | 17 | anass1rs 654 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(๐ ยท ๐ด))) |
19 | | zaddcl 12544 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + ๐) โ โค) |
20 | 19 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐ + ๐) โ โค) |
21 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ + ๐) โ (๐ฅ ยท ๐ด) = ((๐ + ๐) ยท ๐ด)) |
22 | | ovex 7391 |
. . . . . . . . . . . . 13
โข ((๐ + ๐) ยท ๐ด) โ V |
23 | 21, 6, 22 | fvmpt 6949 |
. . . . . . . . . . . 12
โข ((๐ + ๐) โ โค โ (๐นโ(๐ + ๐)) = ((๐ + ๐) ยท ๐ด)) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐นโ(๐ + ๐)) = ((๐ + ๐) ยท ๐ด)) |
25 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐ด) = (๐ ยท ๐ด)) |
26 | | ovex 7391 |
. . . . . . . . . . . . . 14
โข (๐ ยท ๐ด) โ V |
27 | 25, 6, 26 | fvmpt 6949 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐นโ๐) = (๐ ยท ๐ด)) |
28 | 27 | ad2antrl 727 |
. . . . . . . . . . . 12
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐นโ๐) = (๐ ยท ๐ด)) |
29 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐ด) = (๐ ยท ๐ด)) |
30 | | ovex 7391 |
. . . . . . . . . . . . . 14
โข (๐ ยท ๐ด) โ V |
31 | 29, 6, 30 | fvmpt 6949 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐นโ๐) = (๐ ยท ๐ด)) |
32 | 31 | ad2antll 728 |
. . . . . . . . . . . 12
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐นโ๐) = (๐ ยท ๐ด)) |
33 | 28, 32 | oveq12d 7376 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) = ((๐ ยท ๐ด)(+gโ๐บ)(๐ ยท ๐ด))) |
34 | 18, 24, 33 | 3eqtr4d 2787 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐นโ(๐ + ๐)) = ((๐นโ๐)(+gโ๐บ)(๐นโ๐))) |
35 | | fnfvelrn 7032 |
. . . . . . . . . . 11
โข ((๐น Fn โค โง (๐ + ๐) โ โค) โ (๐นโ(๐ + ๐)) โ ran ๐น) |
36 | 9, 19, 35 | syl2an 597 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ (๐นโ(๐ + ๐)) โ ran ๐น) |
37 | 34, 36 | eqeltrrd 2839 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ด โ ๐) โง (๐ โ โค โง ๐ โ โค)) โ ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น) |
38 | 37 | anassrs 469 |
. . . . . . . 8
โข ((((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โง ๐ โ โค) โ ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น) |
39 | 38 | ralrimiva 3144 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ โ๐ โ โค ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น) |
40 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ฃ = (๐นโ๐) โ ((๐นโ๐)(+gโ๐บ)๐ฃ) = ((๐นโ๐)(+gโ๐บ)(๐นโ๐))) |
41 | 40 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ฃ = (๐นโ๐) โ (((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โ ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น)) |
42 | 41 | ralrn 7039 |
. . . . . . . . 9
โข (๐น Fn โค โ
(โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โ โ๐ โ โค ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น)) |
43 | 9, 42 | syl 17 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โ โ๐ โ โค ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น)) |
44 | 43 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โ โ๐ โ โค ((๐นโ๐)(+gโ๐บ)(๐นโ๐)) โ ran ๐น)) |
45 | 39, 44 | mpbird 257 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น) |
46 | | eqid 2737 |
. . . . . . . . . . 11
โข
(invgโ๐บ) = (invgโ๐บ) |
47 | 1, 2, 46 | mulgneg 18895 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ด โ ๐) โ (-๐ ยท ๐ด) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
48 | 47 | 3expa 1119 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ โ โค) โง ๐ด โ ๐) โ (-๐ ยท ๐ด) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
49 | 48 | an32s 651 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (-๐ ยท ๐ด) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
50 | | znegcl 12539 |
. . . . . . . . . 10
โข (๐ โ โค โ -๐ โ
โค) |
51 | 50 | adantl 483 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ -๐ โ โค) |
52 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ฅ = -๐ โ (๐ฅ ยท ๐ด) = (-๐ ยท ๐ด)) |
53 | | ovex 7391 |
. . . . . . . . . 10
โข (-๐ ยท ๐ด) โ V |
54 | 52, 6, 53 | fvmpt 6949 |
. . . . . . . . 9
โข (-๐ โ โค โ (๐นโ-๐) = (-๐ ยท ๐ด)) |
55 | 51, 54 | syl 17 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (๐นโ-๐) = (-๐ ยท ๐ด)) |
56 | 27 | adantl 483 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (๐นโ๐) = (๐ ยท ๐ด)) |
57 | 56 | fveq2d 6847 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ
((invgโ๐บ)โ(๐นโ๐)) = ((invgโ๐บ)โ(๐ ยท ๐ด))) |
58 | 49, 55, 57 | 3eqtr4d 2787 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (๐นโ-๐) = ((invgโ๐บ)โ(๐นโ๐))) |
59 | | fnfvelrn 7032 |
. . . . . . . 8
โข ((๐น Fn โค โง -๐ โ โค) โ (๐นโ-๐) โ ran ๐น) |
60 | 9, 50, 59 | syl2an 597 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (๐นโ-๐) โ ran ๐น) |
61 | 58, 60 | eqeltrrd 2839 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ
((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น) |
62 | 45, 61 | jca 513 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ โ โค) โ (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น)) |
63 | 62 | ralrimiva 3144 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ โ๐ โ โค (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น)) |
64 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ข = (๐นโ๐) โ (๐ข(+gโ๐บ)๐ฃ) = ((๐นโ๐)(+gโ๐บ)๐ฃ)) |
65 | 64 | eleq1d 2823 |
. . . . . . . 8
โข (๐ข = (๐นโ๐) โ ((๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โ ((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น)) |
66 | 65 | ralbidv 3175 |
. . . . . . 7
โข (๐ข = (๐นโ๐) โ (โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โ โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น)) |
67 | | fveq2 6843 |
. . . . . . . 8
โข (๐ข = (๐นโ๐) โ ((invgโ๐บ)โ๐ข) = ((invgโ๐บ)โ(๐นโ๐))) |
68 | 67 | eleq1d 2823 |
. . . . . . 7
โข (๐ข = (๐นโ๐) โ (((invgโ๐บ)โ๐ข) โ ran ๐น โ ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น)) |
69 | 66, 68 | anbi12d 632 |
. . . . . 6
โข (๐ข = (๐นโ๐) โ ((โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น) โ (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น))) |
70 | 69 | ralrn 7039 |
. . . . 5
โข (๐น Fn โค โ
(โ๐ข โ ran ๐น(โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น) โ โ๐ โ โค (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น))) |
71 | 9, 70 | syl 17 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (โ๐ข โ ran ๐น(โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น) โ โ๐ โ โค (โ๐ฃ โ ran ๐น((๐นโ๐)(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ(๐นโ๐)) โ ran ๐น))) |
72 | 63, 71 | mpbird 257 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ โ๐ข โ ran ๐น(โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น)) |
73 | 1, 15, 46 | issubg2 18944 |
. . . 4
โข (๐บ โ Grp โ (ran ๐น โ (SubGrpโ๐บ) โ (ran ๐น โ ๐ โง ran ๐น โ โ
โง โ๐ข โ ran ๐น(โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น)))) |
74 | 73 | adantr 482 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (ran ๐น โ (SubGrpโ๐บ) โ (ran ๐น โ ๐ โง ran ๐น โ โ
โง โ๐ข โ ran ๐น(โ๐ฃ โ ran ๐น(๐ข(+gโ๐บ)๐ฃ) โ ran ๐น โง ((invgโ๐บ)โ๐ข) โ ran ๐น)))) |
75 | 8, 13, 72, 74 | mpbir3and 1343 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ran ๐น โ (SubGrpโ๐บ)) |
76 | | oveq1 7365 |
. . . . . 6
โข (๐ฅ = 1 โ (๐ฅ ยท ๐ด) = (1 ยท ๐ด)) |
77 | | ovex 7391 |
. . . . . 6
โข (1 ยท ๐ด) โ V |
78 | 76, 6, 77 | fvmpt 6949 |
. . . . 5
โข (1 โ
โค โ (๐นโ1)
= (1 ยท ๐ด)) |
79 | 10, 78 | ax-mp 5 |
. . . 4
โข (๐นโ1) = (1 ยท ๐ด) |
80 | 1, 2 | mulg1 18884 |
. . . . 5
โข (๐ด โ ๐ โ (1 ยท ๐ด) = ๐ด) |
81 | 80 | adantl 483 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (1 ยท ๐ด) = ๐ด) |
82 | 79, 81 | eqtrid 2789 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐นโ1) = ๐ด) |
83 | 82, 12 | eqeltrrd 2839 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐) โ ๐ด โ ran ๐น) |
84 | 75, 83 | jca 513 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (ran ๐น โ (SubGrpโ๐บ) โง ๐ด โ ran ๐น)) |