Metamath Proof Explorer


Theorem mulgfvalALT

Description: Shorter proof of mulgfval using ax-rep . (Contributed by Mario Carneiro, 11-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mulgval.b 𝐵 = ( Base ‘ 𝐺 )
mulgval.p + = ( +g𝐺 )
mulgval.o 0 = ( 0g𝐺 )
mulgval.i 𝐼 = ( invg𝐺 )
mulgval.t · = ( .g𝐺 )
Assertion mulgfvalALT · = ( 𝑛 ∈ ℤ , 𝑥𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )

Proof

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 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )