Step |
Hyp |
Ref |
Expression |
1 |
|
mulgval.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
mulgval.p |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
mulgval.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
4 |
|
mulgval.i |
⊢ 𝐼 = ( invg ‘ 𝐺 ) |
5 |
|
mulgval.t |
⊢ · = ( .g ‘ 𝐺 ) |
6 |
|
eqidd |
⊢ ( 𝑤 = 𝐺 → ℤ = ℤ ) |
7 |
|
fveq2 |
⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) ) |
8 |
7 1
|
eqtr4di |
⊢ ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = 𝐵 ) |
9 |
|
fveq2 |
⊢ ( 𝑤 = 𝐺 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝐺 ) ) |
10 |
9 3
|
eqtr4di |
⊢ ( 𝑤 = 𝐺 → ( 0g ‘ 𝑤 ) = 0 ) |
11 |
|
seqex |
⊢ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ∈ V |
12 |
11
|
a1i |
⊢ ( 𝑤 = 𝐺 → seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ∈ V ) |
13 |
|
id |
⊢ ( 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) → 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) |
14 |
|
fveq2 |
⊢ ( 𝑤 = 𝐺 → ( +g ‘ 𝑤 ) = ( +g ‘ 𝐺 ) ) |
15 |
14 2
|
eqtr4di |
⊢ ( 𝑤 = 𝐺 → ( +g ‘ 𝑤 ) = + ) |
16 |
15
|
seqeq2d |
⊢ ( 𝑤 = 𝐺 → seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) = seq 1 ( + , ( ℕ × { 𝑥 } ) ) ) |
17 |
13 16
|
sylan9eqr |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → 𝑠 = seq 1 ( + , ( ℕ × { 𝑥 } ) ) ) |
18 |
17
|
fveq1d |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( 𝑠 ‘ 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ) |
19 |
|
simpl |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → 𝑤 = 𝐺 ) |
20 |
19
|
fveq2d |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( invg ‘ 𝑤 ) = ( invg ‘ 𝐺 ) ) |
21 |
20 4
|
eqtr4di |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( invg ‘ 𝑤 ) = 𝐼 ) |
22 |
17
|
fveq1d |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( 𝑠 ‘ - 𝑛 ) = ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) |
23 |
21 22
|
fveq12d |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) = ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) |
24 |
18 23
|
ifeq12d |
⊢ ( ( 𝑤 = 𝐺 ∧ 𝑠 = seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) ) → if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) |
25 |
12 24
|
csbied |
⊢ ( 𝑤 = 𝐺 → ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) = if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) |
26 |
10 25
|
ifeq12d |
⊢ ( 𝑤 = 𝐺 → if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) = if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) |
27 |
6 8 26
|
mpoeq123dv |
⊢ ( 𝑤 = 𝐺 → ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) ) |
28 |
|
df-mulg |
⊢ .g = ( 𝑤 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑤 ) , ⦋ seq 1 ( ( +g ‘ 𝑤 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑤 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) ) |
29 |
|
zex |
⊢ ℤ ∈ V |
30 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
31 |
29 30
|
mpoex |
⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) ∈ V |
32 |
27 28 31
|
fvmpt |
⊢ ( 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) ) |
33 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ∅ ) |
34 |
|
eqid |
⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) |
35 |
3
|
fvexi |
⊢ 0 ∈ V |
36 |
|
fvex |
⊢ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) ∈ V |
37 |
|
fvex |
⊢ ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ∈ V |
38 |
36 37
|
ifex |
⊢ if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ∈ V |
39 |
35 38
|
ifex |
⊢ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ∈ V |
40 |
34 39
|
fnmpoi |
⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ( ℤ × 𝐵 ) |
41 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ ) |
42 |
1 41
|
eqtrid |
⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ ) |
43 |
42
|
xpeq2d |
⊢ ( ¬ 𝐺 ∈ V → ( ℤ × 𝐵 ) = ( ℤ × ∅ ) ) |
44 |
|
xp0 |
⊢ ( ℤ × ∅ ) = ∅ |
45 |
43 44
|
eqtrdi |
⊢ ( ¬ 𝐺 ∈ V → ( ℤ × 𝐵 ) = ∅ ) |
46 |
45
|
fneq2d |
⊢ ( ¬ 𝐺 ∈ V → ( ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ( ℤ × 𝐵 ) ↔ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ ) ) |
47 |
40 46
|
mpbii |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ ) |
48 |
|
fn0 |
⊢ ( ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) Fn ∅ ↔ ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ∅ ) |
49 |
47 48
|
sylib |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) = ∅ ) |
50 |
33 49
|
eqtr4d |
⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) ) |
51 |
32 50
|
pm2.61i |
⊢ ( .g ‘ 𝐺 ) = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) |
52 |
5 51
|
eqtri |
⊢ · = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) ) |