![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulg0 | Structured version Visualization version GIF version |
Description: Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.) |
Ref | Expression |
---|---|
mulg0.b | ⊢ 𝐵 = (Base‘𝐺) |
mulg0.o | ⊢ 0 = (0g‘𝐺) |
mulg0.t | ⊢ · = (.g‘𝐺) |
Ref | Expression |
---|---|
mulg0 | ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z 12622 | . 2 ⊢ 0 ∈ ℤ | |
2 | mulg0.b | . . . 4 ⊢ 𝐵 = (Base‘𝐺) | |
3 | eqid 2735 | . . . 4 ⊢ (+g‘𝐺) = (+g‘𝐺) | |
4 | mulg0.o | . . . 4 ⊢ 0 = (0g‘𝐺) | |
5 | eqid 2735 | . . . 4 ⊢ (invg‘𝐺) = (invg‘𝐺) | |
6 | mulg0.t | . . . 4 ⊢ · = (.g‘𝐺) | |
7 | eqid 2735 | . . . 4 ⊢ seq1((+g‘𝐺), (ℕ × {𝑋})) = seq1((+g‘𝐺), (ℕ × {𝑋})) | |
8 | 2, 3, 4, 5, 6, 7 | mulgval 19102 | . . 3 ⊢ ((0 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = if(0 = 0, 0 , if(0 < 0, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘0), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-0))))) |
9 | eqid 2735 | . . . 4 ⊢ 0 = 0 | |
10 | 9 | iftruei 4538 | . . 3 ⊢ if(0 = 0, 0 , if(0 < 0, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘0), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-0)))) = 0 |
11 | 8, 10 | eqtrdi 2791 | . 2 ⊢ ((0 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = 0 ) |
12 | 1, 11 | mpan 690 | 1 ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ifcif 4531 {csn 4631 class class class wbr 5148 × cxp 5687 ‘cfv 6563 (class class class)co 7431 0cc0 11153 1c1 11154 < clt 11293 -cneg 11491 ℕcn 12264 ℤcz 12611 seqcseq 14039 Basecbs 17245 +gcplusg 17298 0gc0g 17486 invgcminusg 18965 .gcmg 19098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-nn 12265 df-n0 12525 df-z 12612 df-uz 12877 df-seq 14040 df-mulg 19099 |
This theorem is referenced by: ressmulgnn0 19108 mulgnn0gsum 19111 mulgnn0p1 19116 mulgnn0subcl 19118 mulgneg 19123 mulgaddcom 19129 mulginvcom 19130 mulgnn0z 19132 mulgnn0dir 19135 mulgneg2 19139 mulgnn0ass 19141 mhmmulg 19146 submmulg 19149 cycsubm 19233 odid 19571 oddvdsnn0 19577 oddvds 19580 odf1 19595 gexid 19614 mulgnn0di 19858 0cyg 19926 gsumconst 19967 srgmulgass 20235 srgpcomp 20236 srgbinomlem3 20246 srgbinomlem4 20247 srgbinom 20249 mulgass2 20323 lmodvsmmulgdi 20912 cnfldmulg 21434 cnfldexp 21435 freshmansdream 21611 assamulgscmlem1 21937 mplcoe3 22074 mplcoe5 22076 mplbas2 22078 psrbagev1 22119 evlslem3 22122 evlslem1 22124 mhppwdeg 22172 ply1scltm 22300 ply1idvr1 22314 chfacfscmulgsum 22882 chfacfpmmulgsum 22886 cpmadugsumlemF 22898 tmdmulg 24116 clmmulg 25148 dchrptlem2 27324 xrsmulgzz 32994 omndmul2 33072 omndmul 33074 archirng 33178 archirngz 33179 archiabllem1b 33182 archiabllem2c 33185 elrgspnlem1 33232 elrgspnlem2 33233 elrgspnlem3 33234 elrgspnlem4 33235 rprmdvdspow 33541 evl1deg1 33581 evl1deg2 33582 evl1deg3 33583 aks6d1c1p6 42096 idomnnzpownz 42114 aks6d1c5lem2 42120 deg1pow 42123 aks6d1c6isolem1 42156 aks6d1c6lem5 42159 domnexpgn0cl 42510 abvexp 42519 evlsvvvallem 42548 evlsvvval 42550 selvvvval 42572 evlselv 42574 mhphflem 42583 mhphf 42584 lmodvsmdi 48224 |
Copyright terms: Public domain | W3C validator |