Theorem mulg0 19245

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 12673	. 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 19242	. . 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 1570   ∈ wcel 2145  ifcif 4481  {csn 4583   class class class wbr 5102   × cxp 5645  ‘cfv 6527  (class class class)co 7408  0cc0 11171  1c1 11172   < clt 11314  -cneg 11513  ℕcn 12304  ℤcz 12662  seqcseq 14112  Basecbs 17348  +_gcplusg 17389  0_gc0g 17571  inv_gcminusg 19106  ._gcmg 19238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  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 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-nn 12305  df-n0 12576  df-z 12663  df-uz 12935  df-seq 14113  df-mulg 19239

This theorem is used by:  ressmulgnn0  19248  mulgnn0gsum  19251  mulgnn0p1  19256  mulgnn0subcl  19258  mulgneg  19263  mulgaddcom  19269  mulginvcom  19270  mulgnn0z  19272  mulgnn0dir  19275  mulgneg2  19279  mulgnn0ass  19281  mhmmulg  19286  submmulg  19289  cycsubm  19378  odid  19713  oddvdsnn0  19719  oddvds  19722  odf1  19737  gexid  19756  mulgnn0di  20000  0cyg  20068  gsumconst  20109  omndmul2  20308  omndmul  20310  srgmulgass  20404  srgpcomp  20405  srgbinomlem3  20415  srgbinomlem4  20416  srgbinom  20418  mulgass2  20501  lmodvsmmulgdi  21133  cnfldmulg  21671  cnfldexp  21672  freshmansdream  21841  assamulgscmlem1  22168  mplcoe3  22308  mplcoe5  22310  mplbas2  22312  psrbagev1  22347  evlslem3  22350  evlslem1  22352  evlsvvvallem  22361  evlsvvval  22363  selvvvval  22412  mhppwdeg  22432  psdpw  22452  ply1scltm  22561  ply1idvr1  22574  chfacfscmulgsum  23139  chfacfpmmulgsum  23143  cpmadugsumlemF  23155  tmdmulg  24372  clmmulg  25383  dchrptlem2  27555  xrsmulgzz  33503  ressmulgnn0d  33538  archirng  33682  archirngz  33683  archiabllem1b  33686  archiabllem2c  33689  elrgspnlem1  33736  elrgspnlem2  33737  elrgspnlem3  33738  elrgspnlem4  33739  elrgspn  33740  elrgspnsubrunlem1  33741  elrgspnsubrunlem2  33742  rprmdvdspow  33998  evl1deg1  34041  evl1deg2  34042  evl1deg3  34043  evlextv  34107  vieta  34145  aks6d1c1p6  43084  idomnnzpownz  43102  aks6d1c5lem2  43108  deg1pow  43111  aks6d1c6isolem1  43144  aks6d1c6lem5  43147  domnexpgn0cl  43509  abvexp  43518  evlselv  43539  mhphflem  43546  mhphf  43547  lmodvsmdi  49413