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 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
43 42 xpeq2d ⊢ ( ¬ 𝐺 ∈ V → ( ℤ × 𝐵 ) = ( ℤ × ∅ ) )
44 xp0 ⊢ ( ℤ × ∅ ) = ∅
45 43 44 syl6eq ⊢ ( ¬ 𝐺 ∈ 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 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )