MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulgfvalALT Structured version   Visualization version   GIF version

Theorem mulgfvalALT 18834
Description: Shorter proof of mulgfval 18833 using ax-rep 5240. (Contributed by Mario Carneiro, 11-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
mulgval.b ๐ต = (Baseโ€˜๐บ)
mulgval.p + = (+gโ€˜๐บ)
mulgval.o 0 = (0gโ€˜๐บ)
mulgval.i ๐ผ = (invgโ€˜๐บ)
mulgval.t ยท = (.gโ€˜๐บ)
Assertion
Ref Expression
mulgfvalALT ยท = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))))
Distinct variable groups:   ๐‘ฅ, 0 ,๐‘›   ๐‘ฅ,๐ต,๐‘›   ๐‘ฅ, + ,๐‘›   ๐‘ฅ,๐บ,๐‘›   ๐‘ฅ,๐ผ,๐‘›
Allowed substitution hints:   ยท (๐‘ฅ,๐‘›)

Proof of Theorem mulgfvalALT
Dummy variables ๐‘ค ๐‘  are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulgval.t . 2 ยท = (.gโ€˜๐บ)
2 eqidd 2738 . . . . 5 (๐‘ค = ๐บ โ†’ โ„ค = โ„ค)
3 fveq2 6839 . . . . . 6 (๐‘ค = ๐บ โ†’ (Baseโ€˜๐‘ค) = (Baseโ€˜๐บ))
4 mulgval.b . . . . . 6 ๐ต = (Baseโ€˜๐บ)
53, 4eqtr4di 2795 . . . . 5 (๐‘ค = ๐บ โ†’ (Baseโ€˜๐‘ค) = ๐ต)
6 fveq2 6839 . . . . . . 7 (๐‘ค = ๐บ โ†’ (0gโ€˜๐‘ค) = (0gโ€˜๐บ))
7 mulgval.o . . . . . . 7 0 = (0gโ€˜๐บ)
86, 7eqtr4di 2795 . . . . . 6 (๐‘ค = ๐บ โ†’ (0gโ€˜๐‘ค) = 0 )
9 seqex 13862 . . . . . . . 8 seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) โˆˆ V
109a1i 11 . . . . . . 7 (๐‘ค = ๐บ โ†’ seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) โˆˆ V)
11 id 22 . . . . . . . . . 10 (๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) โ†’ ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})))
12 fveq2 6839 . . . . . . . . . . . 12 (๐‘ค = ๐บ โ†’ (+gโ€˜๐‘ค) = (+gโ€˜๐บ))
13 mulgval.p . . . . . . . . . . . 12 + = (+gโ€˜๐บ)
1412, 13eqtr4di 2795 . . . . . . . . . . 11 (๐‘ค = ๐บ โ†’ (+gโ€˜๐‘ค) = + )
1514seqeq2d 13867 . . . . . . . . . 10 (๐‘ค = ๐บ โ†’ seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) = seq1( + , (โ„• ร— {๐‘ฅ})))
1611, 15sylan9eqr 2799 . . . . . . . . 9 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ ๐‘  = seq1( + , (โ„• ร— {๐‘ฅ})))
1716fveq1d 6841 . . . . . . . 8 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ (๐‘ โ€˜๐‘›) = (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›))
18 simpl 483 . . . . . . . . . . 11 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ ๐‘ค = ๐บ)
1918fveq2d 6843 . . . . . . . . . 10 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ (invgโ€˜๐‘ค) = (invgโ€˜๐บ))
20 mulgval.i . . . . . . . . . 10 ๐ผ = (invgโ€˜๐บ)
2119, 20eqtr4di 2795 . . . . . . . . 9 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ (invgโ€˜๐‘ค) = ๐ผ)
2216fveq1d 6841 . . . . . . . . 9 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ (๐‘ โ€˜-๐‘›) = (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))
2321, 22fveq12d 6846 . . . . . . . 8 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›)) = (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))
2417, 23ifeq12d 4505 . . . . . . 7 ((๐‘ค = ๐บ โˆง ๐‘  = seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ}))) โ†’ if(0 < ๐‘›, (๐‘ โ€˜๐‘›), ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›))) = if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))
2510, 24csbied 3891 . . . . . 6 (๐‘ค = ๐บ โ†’ โฆ‹seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) / ๐‘ โฆŒif(0 < ๐‘›, (๐‘ โ€˜๐‘›), ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›))) = if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))
268, 25ifeq12d 4505 . . . . 5 (๐‘ค = ๐บ โ†’ if(๐‘› = 0, (0gโ€˜๐‘ค), โฆ‹seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) / ๐‘ โฆŒif(0 < ๐‘›, (๐‘ โ€˜๐‘›), ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›)))) = if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))))
272, 5, 26mpoeq123dv 7426 . . . 4 (๐‘ค = ๐บ โ†’ (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ (Baseโ€˜๐‘ค) โ†ฆ if(๐‘› = 0, (0gโ€˜๐‘ค), โฆ‹seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) / ๐‘ โฆŒif(0 < ๐‘›, (๐‘ โ€˜๐‘›), ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›))))) = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))))
28 df-mulg 18832 . . . 4 .g = (๐‘ค โˆˆ V โ†ฆ (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ (Baseโ€˜๐‘ค) โ†ฆ if(๐‘› = 0, (0gโ€˜๐‘ค), โฆ‹seq1((+gโ€˜๐‘ค), (โ„• ร— {๐‘ฅ})) / ๐‘ โฆŒif(0 < ๐‘›, (๐‘ โ€˜๐‘›), ((invgโ€˜๐‘ค)โ€˜(๐‘ โ€˜-๐‘›))))))
29 zex 12466 . . . . 5 โ„ค โˆˆ V
304fvexi 6853 . . . . 5 ๐ต โˆˆ V
3129, 30mpoex 8004 . . . 4 (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) โˆˆ V
3227, 28, 31fvmpt 6945 . . 3 (๐บ โˆˆ V โ†’ (.gโ€˜๐บ) = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))))
33 fvprc 6831 . . . 4 (ยฌ ๐บ โˆˆ V โ†’ (.gโ€˜๐บ) = โˆ…)
34 eqid 2737 . . . . . . 7 (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))))
357fvexi 6853 . . . . . . . 8 0 โˆˆ V
36 fvex 6852 . . . . . . . . 9 (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›) โˆˆ V
37 fvex 6852 . . . . . . . . 9 (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)) โˆˆ V
3836, 37ifex 4534 . . . . . . . 8 if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))) โˆˆ V
3935, 38ifex 4534 . . . . . . 7 if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))) โˆˆ V
4034, 39fnmpoi 7994 . . . . . 6 (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) Fn (โ„ค ร— ๐ต)
41 fvprc 6831 . . . . . . . . . 10 (ยฌ ๐บ โˆˆ V โ†’ (Baseโ€˜๐บ) = โˆ…)
424, 41eqtrid 2789 . . . . . . . . 9 (ยฌ ๐บ โˆˆ V โ†’ ๐ต = โˆ…)
4342xpeq2d 5661 . . . . . . . 8 (ยฌ ๐บ โˆˆ V โ†’ (โ„ค ร— ๐ต) = (โ„ค ร— โˆ…))
44 xp0 6108 . . . . . . . 8 (โ„ค ร— โˆ…) = โˆ…
4543, 44eqtrdi 2793 . . . . . . 7 (ยฌ ๐บ โˆˆ V โ†’ (โ„ค ร— ๐ต) = โˆ…)
4645fneq2d 6593 . . . . . 6 (ยฌ ๐บ โˆˆ V โ†’ ((๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) Fn (โ„ค ร— ๐ต) โ†” (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) Fn โˆ…))
4740, 46mpbii 232 . . . . 5 (ยฌ ๐บ โˆˆ V โ†’ (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) Fn โˆ…)
48 fn0 6629 . . . . 5 ((๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) Fn โˆ… โ†” (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) = โˆ…)
4947, 48sylib 217 . . . 4 (ยฌ ๐บ โˆˆ V โ†’ (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))) = โˆ…)
5033, 49eqtr4d 2780 . . 3 (ยฌ ๐บ โˆˆ V โ†’ (.gโ€˜๐บ) = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›))))))
5132, 50pm2.61i 182 . 2 (.gโ€˜๐บ) = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))))
521, 51eqtri 2765 1 ยท = (๐‘› โˆˆ โ„ค, ๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘› = 0, 0 , if(0 < ๐‘›, (seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜๐‘›), (๐ผโ€˜(seq1( + , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘›)))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  Vcvv 3443  โฆ‹csb 3853  โˆ…c0 4280  ifcif 4484  {csn 4584   class class class wbr 5103   ร— cxp 5629   Fn wfn 6488  โ€˜cfv 6493   โˆˆ cmpo 7353  0cc0 11009  1c1 11010   < clt 11147  -cneg 11344  โ„•cn 12111  โ„คcz 12457  seqcseq 13860  Basecbs 17043  +gcplusg 17093  0gc0g 17281  invgcminusg 18709  .gcmg 18831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535  ax-cnex 11065  ax-resscn 11066
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-neg 11346  df-z 12458  df-seq 13861  df-mulg 18832
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator