Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tendo0mul Unicode version

Theorem tendo0mul 34751
Description: Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.)
Hypotheses
Ref Expression
tendoid0.b
tendoid0.h
tendoid0.t
tendoid0.e
tendoid0.o
Assertion
Ref Expression
tendo0mul
Distinct variable groups:   ,   ,

Proof of Theorem tendo0mul
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 tendoid0.b . . . 4
2 tendoid0.h . . . 4
3 tendoid0.t . . . 4
41, 2, 3cdlemftr0 34493 . . 3
54adantr 465 . 2
6 simpll 753 . . 3
7 tendoid0.e . . . . . 6
8 tendoid0.o . . . . . 6
91, 2, 3, 7, 8tendo0cl 34715 . . . . 5
109ad2antrr 725 . . . 4
11 simplr 754 . . . 4
122, 7tendococl 34697 . . . 4
136, 10, 11, 12syl3anc 1219 . . 3
14 simprl 755 . . . . . 6
152, 3, 7tendocl 34692 . . . . . 6
166, 11, 14, 15syl3anc 1219 . . . . 5
178, 1tendo02 34712 . . . . 5
1816, 17syl 16 . . . 4
192, 3, 7tendocoval 34691 . . . . 5
206, 10, 11, 14, 19syl121anc 1224 . . . 4
218, 1tendo02 34712 . . . . 5
2221ad2antrl 727 . . . 4
2318, 20, 223eqtr4d 2500 . . 3
24 simpr 461 . . 3
251, 2, 3, 7tendocan 34749 . . 3
266, 13, 10, 23, 24, 25syl131anc 1232 . 2
275, 26rexlimddv 2925 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1757  =/=wne 2641  E.wrex 2793  e.cmpt 4432   cid 4713  |`cres 4924  o.ccom 4926  `cfv 5500   cbs 14260   chlt 33276   clh 33909   cltrn 34026   ctendo 34677
This theorem is referenced by:  cdleml5N  34905  cdleml9  34909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-riotaBAD 32885
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-iun 4255  df-iin 4256  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-1st 6661  df-2nd 6662  df-undef 6876  df-map 7300  df-poset 15202  df-plt 15214  df-lub 15230  df-glb 15231  df-join 15232  df-meet 15233  df-p0 15295  df-p1 15296  df-lat 15302  df-clat 15364  df-oposet 33102  df-ol 33104  df-oml 33105  df-covers 33192  df-ats 33193  df-atl 33224  df-cvlat 33248  df-hlat 33277  df-llines 33423  df-lplanes 33424  df-lvols 33425  df-lines 33426  df-psubsp 33428  df-pmap 33429  df-padd 33721  df-lhyp 33913  df-laut 33914  df-ldil 34029  df-ltrn 34030  df-trl 34084  df-tendo 34680
  Copyright terms: Public domain W3C validator