Step | Hyp | Ref
| Expression |
1 | | elex 2744 |
. . . . . . 7
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
2 | | fn0g 12656 |
. . . . . . . 8
⊢
0g Fn V |
3 | | funfvex 5521 |
. . . . . . . . 9
⊢ ((Fun
0g ∧ 𝐺
∈ dom 0g) → (0g‘𝐺) ∈ V) |
4 | 3 | funfni 5305 |
. . . . . . . 8
⊢
((0g Fn V ∧ 𝐺 ∈ V) → (0g‘𝐺) ∈ V) |
5 | 2, 4 | mpan 424 |
. . . . . . 7
⊢ (𝐺 ∈ V →
(0g‘𝐺)
∈ V) |
6 | 1, 5 | syl 14 |
. . . . . 6
⊢ (𝐺 ∈ 𝑉 → (0g‘𝐺) ∈ V) |
7 | 6 | ad2antrr 488 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ 𝑛 = 0) → (0g‘𝐺) ∈ V) |
8 | | nnuz 9531 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
9 | | 1zzd 9248 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → 1 ∈ ℤ) |
10 | | fvconst2g 5719 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ ×
{𝑥})‘𝑢) = 𝑥) |
11 | | simpl 109 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → 𝑥 ∈ 𝐵) |
12 | 10, 11 | eqeltrd 2250 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ ×
{𝑥})‘𝑢) ∈ 𝐵) |
13 | 12 | elexd 2746 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ ×
{𝑥})‘𝑢) ∈ V) |
14 | 13 | adantll 476 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ ℕ) → ((ℕ ×
{𝑥})‘𝑢) ∈ V) |
15 | | simprl 529 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → 𝑢 ∈ V) |
16 | | plusgslid 12522 |
. . . . . . . . . . . . 13
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
17 | 16 | slotex 12452 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ 𝑉 → (+g‘𝐺) ∈ V) |
18 | 17 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (+g‘𝐺) ∈ V) |
19 | | simprr 530 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → 𝑣 ∈ V) |
20 | | ovexg 5896 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ V ∧
(+g‘𝐺)
∈ V ∧ 𝑣 ∈ V)
→ (𝑢(+g‘𝐺)𝑣) ∈ V) |
21 | 15, 18, 19, 20 | syl3anc 1236 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (𝑢(+g‘𝐺)𝑣) ∈ V) |
22 | 8, 9, 14, 21 | seqf 10426 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵) → seq1((+g‘𝐺), (ℕ × {𝑥})):ℕ⟶V) |
23 | 22 | adantrl 478 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → seq1((+g‘𝐺), (ℕ × {𝑥})):ℕ⟶V) |
24 | 23 | ad2antrr 488 |
. . . . . . 7
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ 0 < 𝑛) → seq1((+g‘𝐺), (ℕ × {𝑥})):ℕ⟶V) |
25 | | simprl 529 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → 𝑛 ∈ ℤ) |
26 | 25 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ 0 < 𝑛) → 𝑛 ∈ ℤ) |
27 | | simpr 110 |
. . . . . . . 8
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ 0 < 𝑛) → 0 < 𝑛) |
28 | | elnnz 9231 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℤ ∧ 0 <
𝑛)) |
29 | 26, 27, 28 | sylanbrc 417 |
. . . . . . 7
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ 0 < 𝑛) → 𝑛 ∈ ℕ) |
30 | 24, 29 | ffvelrnd 5641 |
. . . . . 6
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ 0 < 𝑛) → (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛) ∈ V) |
31 | | mulgfn.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
32 | | eqid 2173 |
. . . . . . . . . 10
⊢
(invg‘𝐺) = (invg‘𝐺) |
33 | 31, 32 | grpinvfng 12774 |
. . . . . . . . 9
⊢ (𝐺 ∈ 𝑉 → (invg‘𝐺) Fn 𝐵) |
34 | | basfn 12482 |
. . . . . . . . . . . 12
⊢ Base Fn
V |
35 | | funfvex 5521 |
. . . . . . . . . . . . 13
⊢ ((Fun
Base ∧ 𝐺 ∈ dom
Base) → (Base‘𝐺)
∈ V) |
36 | 35 | funfni 5305 |
. . . . . . . . . . . 12
⊢ ((Base Fn
V ∧ 𝐺 ∈ V) →
(Base‘𝐺) ∈
V) |
37 | 34, 36 | mpan 424 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ V →
(Base‘𝐺) ∈
V) |
38 | 31, 37 | eqeltrid 2260 |
. . . . . . . . . 10
⊢ (𝐺 ∈ V → 𝐵 ∈ V) |
39 | 1, 38 | syl 14 |
. . . . . . . . 9
⊢ (𝐺 ∈ 𝑉 → 𝐵 ∈ V) |
40 | | fnex 5727 |
. . . . . . . . 9
⊢
(((invg‘𝐺) Fn 𝐵 ∧ 𝐵 ∈ V) →
(invg‘𝐺)
∈ V) |
41 | 33, 39, 40 | syl2anc 411 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝑉 → (invg‘𝐺) ∈ V) |
42 | 41 | ad3antrrr 492 |
. . . . . . 7
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → (invg‘𝐺) ∈ V) |
43 | 23 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → seq1((+g‘𝐺), (ℕ × {𝑥})):ℕ⟶V) |
44 | 25 | znegcld 9345 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → -𝑛 ∈ ℤ) |
45 | 44 | ad2antrr 488 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → -𝑛 ∈ ℤ) |
46 | | simplr 528 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → ¬ 𝑛 = 0) |
47 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → ¬ 0 < 𝑛) |
48 | | ztri3or0 9263 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (𝑛 < 0 ∨ 𝑛 = 0 ∨ 0 < 𝑛)) |
49 | 25, 48 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → (𝑛 < 0 ∨ 𝑛 = 0 ∨ 0 < 𝑛)) |
50 | 49 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → (𝑛 < 0 ∨ 𝑛 = 0 ∨ 0 < 𝑛)) |
51 | 46, 47, 50 | ecase23d 1348 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → 𝑛 < 0) |
52 | 25 | zred 9343 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → 𝑛 ∈ ℝ) |
53 | 52 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → 𝑛 ∈ ℝ) |
54 | 53 | lt0neg1d 8443 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → (𝑛 < 0 ↔ 0 < -𝑛)) |
55 | 51, 54 | mpbid 148 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → 0 < -𝑛) |
56 | | elnnz 9231 |
. . . . . . . . 9
⊢ (-𝑛 ∈ ℕ ↔ (-𝑛 ∈ ℤ ∧ 0 <
-𝑛)) |
57 | 45, 55, 56 | sylanbrc 417 |
. . . . . . . 8
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → -𝑛 ∈ ℕ) |
58 | 43, 57 | ffvelrnd 5641 |
. . . . . . 7
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → (seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛) ∈ V) |
59 | | fvexg 5523 |
. . . . . . 7
⊢
(((invg‘𝐺) ∈ V ∧
(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛) ∈ V) →
((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)) ∈ V) |
60 | 42, 58, 59 | syl2anc 411 |
. . . . . 6
⊢ ((((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) ∧ ¬ 0 < 𝑛) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)) ∈ V) |
61 | | 0zd 9233 |
. . . . . . 7
⊢ (((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) → 0 ∈
ℤ) |
62 | | simplrl 533 |
. . . . . . 7
⊢ (((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℤ) |
63 | | zdclt 9298 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 𝑛
∈ ℤ) → DECID 0 < 𝑛) |
64 | 61, 62, 63 | syl2anc 411 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) → DECID 0 <
𝑛) |
65 | 30, 60, 64 | ifcldadc 3558 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) ∧ ¬ 𝑛 = 0) → if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))) ∈ V) |
66 | | 0zd 9233 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → 0 ∈ ℤ) |
67 | | zdceq 9296 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 0 ∈
ℤ) → DECID 𝑛 = 0) |
68 | 25, 66, 67 | syl2anc 411 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → DECID 𝑛 = 0) |
69 | 7, 65, 68 | ifcldadc 3558 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ (𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)))) ∈ V) |
70 | 69 | ralrimivva 2555 |
. . 3
⊢ (𝐺 ∈ 𝑉 → ∀𝑛 ∈ ℤ ∀𝑥 ∈ 𝐵 if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)))) ∈ V) |
71 | | eqid 2173 |
. . . 4
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))))) |
72 | 71 | fnmpo 6190 |
. . 3
⊢
(∀𝑛 ∈
ℤ ∀𝑥 ∈
𝐵 if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)))) ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵)) |
73 | 70, 72 | syl 14 |
. 2
⊢ (𝐺 ∈ 𝑉 → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵)) |
74 | | eqid 2173 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
75 | | eqid 2173 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
76 | | mulgfn.t |
. . . 4
⊢ · =
(.g‘𝐺) |
77 | 31, 74, 75, 32, 76 | mulgfvalg 12841 |
. . 3
⊢ (𝐺 ∈ 𝑉 → · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛)))))) |
78 | 77 | fneq1d 5295 |
. 2
⊢ (𝐺 ∈ 𝑉 → ( · Fn (ℤ ×
𝐵) ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, (0g‘𝐺), if(0 < 𝑛, (seq1((+g‘𝐺), (ℕ × {𝑥}))‘𝑛), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵))) |
79 | 73, 78 | mpbird 168 |
1
⊢ (𝐺 ∈ 𝑉 → · Fn (ℤ ×
𝐵)) |