HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cnlnadjlem6 Unicode version

Theorem cnlnadjlem6 25595
Description: Lemma for cnlnadji 25599. is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.1
cnlnadjlem.2
cnlnadjlem.3
cnlnadjlem.4
cnlnadjlem.5
Assertion
Ref Expression
cnlnadjlem6
Distinct variable groups:   , , ,   ,   , , , ,   , ,

Proof of Theorem cnlnadjlem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnlnadjlem.5 . . 3
2 cnlnadjlem.1 . . . 4
3 cnlnadjlem.2 . . . 4
4 cnlnadjlem.3 . . . 4
5 cnlnadjlem.4 . . . 4
62, 3, 4, 5cnlnadjlem3 25592 . . 3
71, 6fmpti 5949 . 2
82lnopfi 25492 . . . . . . . . . 10
98ffvelrni 5925 . . . . . . . . 9
109adantl 466 . . . . . . . 8
11 hvmulcl 24534 . . . . . . . . 9
1211ad2antrr 725 . . . . . . . 8
13 simplr 754 . . . . . . . 8
14 his7 24611 . . . . . . . 8
1510, 12, 13, 14syl3anc 1219 . . . . . . 7
16 hvaddcl 24533 . . . . . . . . 9
1711, 16sylan 471 . . . . . . . 8
182, 3, 4, 5, 1cnlnadjlem5 25594 . . . . . . . 8
1917, 18sylan 471 . . . . . . 7
20 simpll 753 . . . . . . . . . . . 12
219adantl 466 . . . . . . . . . . . 12
22 simplr 754 . . . . . . . . . . . 12
23 his5 24607 . . . . . . . . . . . 12
2420, 21, 22, 23syl3anc 1219 . . . . . . . . . . 11
25 simpr 461 . . . . . . . . . . . . 13
262, 3, 4, 5, 1cnlnadjlem4 25593 . . . . . . . . . . . . . 14
2726ad2antlr 726 . . . . . . . . . . . . 13
28 his5 24607 . . . . . . . . . . . . 13
2920, 25, 27, 28syl3anc 1219 . . . . . . . . . . . 12
302, 3, 4, 5, 1cnlnadjlem5 25594 . . . . . . . . . . . . . 14
3130adantll 713 . . . . . . . . . . . . 13
3231oveq2d 6190 . . . . . . . . . . . 12
3329, 32eqtr4d 2493 . . . . . . . . . . 11
3424, 33eqtr4d 2493 . . . . . . . . . 10
3534adantlr 714 . . . . . . . . 9
362, 3, 4, 5, 1cnlnadjlem5 25594 . . . . . . . . . 10
3736adantll 713 . . . . . . . . 9
3835, 37oveq12d 6192 . . . . . . . 8
39 simpr 461 . . . . . . . . 9
40 hvmulcl 24534 . . . . . . . . . . 11
4126, 40sylan2 474 . . . . . . . . . 10
4241ad2antrr 725 . . . . . . . . 9
432, 3, 4, 5, 1cnlnadjlem4 25593 . . . . . . . . . 10
4443ad2antlr 726 . . . . . . . . 9
45 his7 24611 . . . . . . . . 9
4639, 42, 44, 45syl3anc 1219 . . . . . . . 8
4738, 46eqtr4d 2493 . . . . . . 7
4815, 19, 473eqtr3d 2498 . . . . . 6
4948ralrimiva 2879 . . . . 5
502, 3, 4, 5, 1cnlnadjlem4 25593 . . . . . . 7
5117, 50syl 16 . . . . . 6
52 hvaddcl 24533 . . . . . . 7
5341, 43, 52syl2an 477 . . . . . 6
54 hial2eq2 24628 . . . . . 6
5551, 53, 54syl2anc 661 . . . . 5
5649, 55mpbid 210 . . . 4
5756ralrimiva 2879 . . 3
5857rgen2 2892 . 2
59 ellnop 25381 . 2
607, 58, 59mpbir2an 911 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1757  A.wral 2792  e.cmpt 4432  -->wf 5496  `cfv 5500  iota_crio 6134  (class class class)co 6174   cc 9365   caddc 9370   cmul 9372   ccj 12671   chil 24440   cva 24441   csm 24442   csp 24443   ccop 24467   clo 24468
This theorem is referenced by:  cnlnadjlem8  25597  cnlnadjlem9  25598
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-inf2 7932  ax-cc 8689  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444  ax-pre-sup 9445  ax-addf 9446  ax-mulf 9447  ax-hilex 24520  ax-hfvadd 24521  ax-hvcom 24522  ax-hvass 24523  ax-hv0cl 24524  ax-hvaddid 24525  ax-hfvmul 24526  ax-hvmulid 24527  ax-hvmulass 24528  ax-hvdistr1 24529  ax-hvdistr2 24530  ax-hvmul0 24531  ax-hfi 24600  ax-his1 24603  ax-his2 24604  ax-his3 24605  ax-his4 24606  ax-hcompl 24723
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-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-iin 4256  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-se 4762  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  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-isom 5509  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-of 6404  df-om 6561  df-1st 6661  df-2nd 6662  df-supp 6775  df-recs 6916  df-rdg 6950  df-1o 7004  df-2o 7005  df-oadd 7008  df-omul 7009  df-er 7185  df-map 7300  df-pm 7301  df-ixp 7348  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-fsupp 7706  df-fi 7746  df-sup 7776  df-oi 7809  df-card 8194  df-acn 8197  df-cda 8422  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-div 10079  df-nn 10408  df-2 10465  df-3 10466  df-4 10467  df-5 10468  df-6 10469  df-7 10470  df-8 10471  df-9 10472  df-10 10473  df-n0 10665  df-z 10732  df-dec 10841  df-uz 10947  df-q 11039  df-rp 11077  df-xneg 11174  df-xadd 11175  df-xmul 11176  df-ioo 11389  df-ico 11391  df-icc 11392  df-fz 11523  df-fzo 11634  df-fl 11727  df-seq 11892  df-exp 11951  df-hash 12189  df-cj 12674  df-re 12675  df-im 12676  df-sqr 12810  df-abs 12811  df-clim 13052  df-rlim 13053  df-sum 13250  df-struct 14262  df-ndx 14263  df-slot 14264  df-base 14265  df-sets 14266  df-ress 14267  df-plusg 14337  df-mulr 14338  df-starv 14339  df-sca 14340  df-vsca 14341  df-ip 14342  df-tset 14343  df-ple 14344  df-ds 14346  df-unif 14347  df-hom 14348  df-cco 14349  df-rest 14447  df-topn 14448  df-0g 14466  df-gsum 14467  df-topgen 14468  df-pt 14469  df-prds 14472  df-xrs 14526  df-qtop 14531  df-imas 14532  df-xps 14534  df-mre 14610  df-mrc 14611  df-acs 14613  df-mnd 15501  df-submnd 15551  df-mulg 15634  df-cntz 15921  df-cmn 16367  df-psmet 17902  df-xmet 17903  df-met 17904  df-bl 17905  df-mopn 17906  df-fbas 17907  df-fg 17908  df-cnfld 17912  df-top 18603  df-bases 18605  df-topon 18606  df-topsp 18607  df-cld 18723  df-ntr 18724  df-cls 18725  df-nei 18802  df-cn 18931  df-cnp 18932  df-lm 18933  df-t1 19018  df-haus 19019  df-tx 19235  df-hmeo 19428  df-fil 19519  df-fm 19611  df-flim 19612  df-flf 19613  df-xms 19995  df-ms 19996  df-tms 19997  df-cfil 20866  df-cau 20867  df-cmet 20868  df-grpo 23797  df-gid 23798  df-ginv 23799  df-gdiv 23800  df-ablo 23888  df-subgo 23908  df-vc 24043  df-nv 24089  df-va 24092  df-ba 24093  df-sm 24094  df-0v 24095  df-vs 24096  df-nmcv 24097  df-ims 24098  df-dip 24215  df-ssp 24239  df-ph 24332  df-cbn 24383  df-hnorm 24489  df-hba 24490  df-hvsub 24492  df-hlim 24493  df-hcau 24494  df-sh 24728  df-ch 24743  df-oc 24774  df-ch0 24775  df-nmop 25362  df-cnop 25363  df-lnop 25364  df-nmfn 25368  df-nlfn 25369  df-cnfn 25370  df-lnfn 25371
  Copyright terms: Public domain W3C validator