Step | Hyp | Ref
| Expression |
1 | | cycsubg.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
2 | | cycsubg.t |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
3 | 1, 2 | mulgcl 17559 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
4 | 3 | 3expa 1265 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ) ∧ 𝐴 ∈ 𝑋) → (𝑥 · 𝐴) ∈ 𝑋) |
5 | 4 | an32s 846 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝐴) ∈ 𝑋) |
6 | | cycsubg.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) |
7 | 5, 6 | fmptd 6385 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → 𝐹:ℤ⟶𝑋) |
8 | | frn 6053 |
. . . 4
⊢ (𝐹:ℤ⟶𝑋 → ran 𝐹 ⊆ 𝑋) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ⊆ 𝑋) |
10 | | 1z 11407 |
. . . . . . 7
⊢ 1 ∈
ℤ |
11 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑥 · 𝐴) = (1 · 𝐴)) |
12 | | ovex 6678 |
. . . . . . . 8
⊢ (1 · 𝐴) ∈ V |
13 | 11, 6, 12 | fvmpt 6282 |
. . . . . . 7
⊢ (1 ∈
ℤ → (𝐹‘1)
= (1 · 𝐴)) |
14 | 10, 13 | ax-mp 5 |
. . . . . 6
⊢ (𝐹‘1) = (1 · 𝐴) |
15 | 1, 2 | mulg1 17548 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (1 · 𝐴) = 𝐴) |
16 | 15 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (1 · 𝐴) = 𝐴) |
17 | 14, 16 | syl5eq 2668 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹‘1) = 𝐴) |
18 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:ℤ⟶𝑋 → 𝐹 Fn ℤ) |
19 | 7, 18 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → 𝐹 Fn ℤ) |
20 | | fnfvelrn 6356 |
. . . . . 6
⊢ ((𝐹 Fn ℤ ∧ 1 ∈
ℤ) → (𝐹‘1)
∈ ran 𝐹) |
21 | 19, 10, 20 | sylancl 694 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹‘1) ∈ ran 𝐹) |
22 | 17, 21 | eqeltrrd 2702 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ ran 𝐹) |
23 | | ne0i 3921 |
. . . 4
⊢ (𝐴 ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
24 | 22, 23 | syl 17 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ≠ ∅) |
25 | | df-3an 1039 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ 𝑋) ↔ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝐴 ∈ 𝑋)) |
26 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐺) = (+g‘𝐺) |
27 | 1, 2, 26 | mulgdir 17573 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ 𝑋)) → ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴)(+g‘𝐺)(𝑛 · 𝐴))) |
28 | 25, 27 | sylan2br 493 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝐴 ∈ 𝑋)) → ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴)(+g‘𝐺)(𝑛 · 𝐴))) |
29 | 28 | anass1rs 849 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴)(+g‘𝐺)(𝑛 · 𝐴))) |
30 | | zaddcl 11417 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 + 𝑛) ∈ ℤ) |
31 | 30 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑚 + 𝑛) ∈ ℤ) |
32 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑚 + 𝑛) → (𝑥 · 𝐴) = ((𝑚 + 𝑛) · 𝐴)) |
33 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ ((𝑚 + 𝑛) · 𝐴) ∈ V |
34 | 32, 6, 33 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ ((𝑚 + 𝑛) ∈ ℤ → (𝐹‘(𝑚 + 𝑛)) = ((𝑚 + 𝑛) · 𝐴)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐹‘(𝑚 + 𝑛)) = ((𝑚 + 𝑛) · 𝐴)) |
36 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑚 → (𝑥 · 𝐴) = (𝑚 · 𝐴)) |
37 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑚 · 𝐴) ∈ V |
38 | 36, 6, 37 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℤ → (𝐹‘𝑚) = (𝑚 · 𝐴)) |
39 | 38 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐹‘𝑚) = (𝑚 · 𝐴)) |
40 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → (𝑥 · 𝐴) = (𝑛 · 𝐴)) |
41 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑛 · 𝐴) ∈ V |
42 | 40, 6, 41 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (𝐹‘𝑛) = (𝑛 · 𝐴)) |
43 | 42 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐹‘𝑛) = (𝑛 · 𝐴)) |
44 | 39, 43 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) = ((𝑚 · 𝐴)(+g‘𝐺)(𝑛 · 𝐴))) |
45 | 29, 35, 44 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐹‘(𝑚 + 𝑛)) = ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛))) |
46 | | fnfvelrn 6356 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn ℤ ∧ (𝑚 + 𝑛) ∈ ℤ) → (𝐹‘(𝑚 + 𝑛)) ∈ ran 𝐹) |
47 | 19, 30, 46 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐹‘(𝑚 + 𝑛)) ∈ ran 𝐹) |
48 | 45, 47 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹) |
49 | 48 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹) |
50 | 49 | ralrimiva 2966 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → ∀𝑛 ∈ ℤ ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹) |
51 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝐹‘𝑛) → ((𝐹‘𝑚)(+g‘𝐺)𝑣) = ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛))) |
52 | 51 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑣 = (𝐹‘𝑛) → (((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹)) |
53 | 52 | ralrn 6362 |
. . . . . . . . 9
⊢ (𝐹 Fn ℤ →
(∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ∀𝑛 ∈ ℤ ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹)) |
54 | 19, 53 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ∀𝑛 ∈ ℤ ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹)) |
55 | 54 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ∀𝑛 ∈ ℤ ((𝐹‘𝑚)(+g‘𝐺)(𝐹‘𝑛)) ∈ ran 𝐹)) |
56 | 50, 55 | mpbird 247 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → ∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹) |
57 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
58 | 1, 2, 57 | mulgneg 17560 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → (-𝑚 · 𝐴) = ((invg‘𝐺)‘(𝑚 · 𝐴))) |
59 | 58 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ∈ 𝑋) → (-𝑚 · 𝐴) = ((invg‘𝐺)‘(𝑚 · 𝐴))) |
60 | 59 | an32s 846 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (-𝑚 · 𝐴) = ((invg‘𝐺)‘(𝑚 · 𝐴))) |
61 | | znegcl 11412 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → -𝑚 ∈
ℤ) |
62 | 61 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → -𝑚 ∈ ℤ) |
63 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑚 → (𝑥 · 𝐴) = (-𝑚 · 𝐴)) |
64 | | ovex 6678 |
. . . . . . . . . 10
⊢ (-𝑚 · 𝐴) ∈ V |
65 | 63, 6, 64 | fvmpt 6282 |
. . . . . . . . 9
⊢ (-𝑚 ∈ ℤ → (𝐹‘-𝑚) = (-𝑚 · 𝐴)) |
66 | 62, 65 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (𝐹‘-𝑚) = (-𝑚 · 𝐴)) |
67 | 38 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) = (𝑚 · 𝐴)) |
68 | 67 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) →
((invg‘𝐺)‘(𝐹‘𝑚)) = ((invg‘𝐺)‘(𝑚 · 𝐴))) |
69 | 60, 66, 68 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (𝐹‘-𝑚) = ((invg‘𝐺)‘(𝐹‘𝑚))) |
70 | | fnfvelrn 6356 |
. . . . . . . 8
⊢ ((𝐹 Fn ℤ ∧ -𝑚 ∈ ℤ) → (𝐹‘-𝑚) ∈ ran 𝐹) |
71 | 19, 61, 70 | syl2an 494 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (𝐹‘-𝑚) ∈ ran 𝐹) |
72 | 69, 71 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) →
((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹) |
73 | 56, 72 | jca 554 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) ∧ 𝑚 ∈ ℤ) → (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹)) |
74 | 73 | ralrimiva 2966 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ∀𝑚 ∈ ℤ (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹)) |
75 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑢 = (𝐹‘𝑚) → (𝑢(+g‘𝐺)𝑣) = ((𝐹‘𝑚)(+g‘𝐺)𝑣)) |
76 | 75 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑢 = (𝐹‘𝑚) → ((𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹)) |
77 | 76 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑚) → (∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ↔ ∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹)) |
78 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑢 = (𝐹‘𝑚) → ((invg‘𝐺)‘𝑢) = ((invg‘𝐺)‘(𝐹‘𝑚))) |
79 | 78 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑢 = (𝐹‘𝑚) → (((invg‘𝐺)‘𝑢) ∈ ran 𝐹 ↔ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹)) |
80 | 77, 79 | anbi12d 747 |
. . . . . 6
⊢ (𝑢 = (𝐹‘𝑚) → ((∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹) ↔ (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹))) |
81 | 80 | ralrn 6362 |
. . . . 5
⊢ (𝐹 Fn ℤ →
(∀𝑢 ∈ ran 𝐹(∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹) ↔ ∀𝑚 ∈ ℤ (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹))) |
82 | 19, 81 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (∀𝑢 ∈ ran 𝐹(∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹) ↔ ∀𝑚 ∈ ℤ (∀𝑣 ∈ ran 𝐹((𝐹‘𝑚)(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘(𝐹‘𝑚)) ∈ ran 𝐹))) |
83 | 74, 82 | mpbird 247 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ∀𝑢 ∈ ran 𝐹(∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹)) |
84 | 1, 26, 57 | issubg2 17609 |
. . . 4
⊢ (𝐺 ∈ Grp → (ran 𝐹 ∈ (SubGrp‘𝐺) ↔ (ran 𝐹 ⊆ 𝑋 ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑢 ∈ ran 𝐹(∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹)))) |
85 | 84 | adantr 481 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (ran 𝐹 ∈ (SubGrp‘𝐺) ↔ (ran 𝐹 ⊆ 𝑋 ∧ ran 𝐹 ≠ ∅ ∧ ∀𝑢 ∈ ran 𝐹(∀𝑣 ∈ ran 𝐹(𝑢(+g‘𝐺)𝑣) ∈ ran 𝐹 ∧ ((invg‘𝐺)‘𝑢) ∈ ran 𝐹)))) |
86 | 9, 24, 83, 85 | mpbir3and 1245 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺)) |
87 | 86, 22 | jca 554 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (ran 𝐹 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ran 𝐹)) |