Theorem mulg0 19284

Description: Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)

Hypotheses

Ref	Expression
mulg0.b	⊢ 𝐵 = (Base‘𝐺)
mulg0.o	⊢ 0 = (0g‘𝐺)
mulg0.t	⊢ · = (.g‘𝐺)

Assertion

Ref	Expression
mulg0	⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 )

Proof of Theorem mulg0

Step	Hyp	Ref	Expression
1		0z 12704	. 2 ⊢ 0 ∈ ℤ
2		mulg0.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
3		eqid 2760	. . . 4 ⊢ (+g‘𝐺) = (+g‘𝐺)
4		mulg0.o	. . . 4 ⊢ 0 = (0g‘𝐺)
5		eqid 2760	. . . 4 ⊢ (invg‘𝐺) = (invg‘𝐺)
6		mulg0.t	. . . 4 ⊢ · = (.g‘𝐺)
7		eqid 2760	. . . 4 ⊢ seq1((+g‘𝐺), (ℕ × {𝑋})) = seq1((+g‘𝐺), (ℕ × {𝑋}))
8	2, 3, 4, 5, 6, 7	mulgval 19281	. . 3 ⊢ ((0 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = if(0 = 0, 0 , if(0 < 0, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘0), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘ -0)))))
9		eqid 2760	. . . 4 ⊢ 0 = 0
10	9	iftruei 4488	. . 3 ⊢ if(0 = 0, 0 , if(0 < 0, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘0), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘ -0)))) = 0
11	8, 10	eqtrdi 2811	. 2 ⊢ ((0 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = 0 )
12	1, 11	mpan 703	1 ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 )

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ifcif 4481  {csn 4583   class class class wbr 5102   × cxp 5648  ‘cfv 6538  (class class class)co 7420  0cc0 11200  1c1 11201   < clt 11343   -cneg 11542  ℕcn 12335  ℤcz 12693  seqcseq 14144  Basecbs 17387  +_gcplusg 17428  0_gc0g 17610  inv_gcminusg 19145  ._gcmg 19277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-uz 12966  df-seq 14145  df-mulg 19278

This theorem is used by:  ressmulgnn0  19287  mulgnn0gsum  19290  mulgnn0p1  19295  mulgnn0subcl  19297  mulgneg  19302  mulgaddcom  19308  mulginvcom  19309  mulgnn0z  19311  mulgnn0dir  19314  mulgneg2  19318  mulgnn0ass  19320  mhmmulg  19325  submmulg  19328  cycsubm  19417  odid  19752  oddvdsnn0  19758  oddvds  19761  odf1  19776  gexid  19795  mulgnn0di  20039  0cyg  20107  gsumconst  20148  omndmul2  20347  omndmul  20349  srgmulgass  20443  srgpcomp  20444  srgbinomlem3  20454  srgbinomlem4  20455  srgbinom  20457  mulgass2  20540  lmodvsmmulgdi  21172  cnfldmulg  21710  cnfldexp  21711  freshmansdream  21880  assamulgscmlem1  22207  mplcoe3  22347  mplcoe5  22349  mplbas2  22351  psrbagev1  22386  evlslem3  22389  evlslem1  22391  evlsvvvallem  22400  evlsvvval  22402  selvvvval  22451  mhppwdeg  22471  psdpw  22491  ply1scltm  22600  ply1idvr1  22613  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  cpmadugsumlemF  23194  tmdmulg  24411  clmmulg  25422  dchrptlem2  27592  xrsmulgzz  33612  ressmulgnn0d  33647  archirng  33791  archirngz  33792  archiabllem1b  33795  archiabllem2c  33798  elrgspnlem1  33845  elrgspnlem2  33846  elrgspnlem3  33847  elrgspnlem4  33848  elrgspn  33849  elrgspnsubrunlem1  33850  elrgspnsubrunlem2  33851  rprmdvdspow  34107  evl1deg1  34150  evl1deg2  34151  evl1deg3  34152  evlextv  34216  vieta  34254  aks6d1c1p6  43207  idomnnzpownz  43225  aks6d1c5lem2  43231  deg1pow  43234  aks6d1c6isolem1  43267  aks6d1c6lem5  43270  domnexpgn0cl  43627  abvexp  43639  evlselv  43660  mhphflem  43667  mhphf  43668  lmodvsmdi  49534