Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspph Structured version   Unicode version

Theorem sspph 26472
 Description: A subspace of an inner product space is an inner product space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
Hypothesis
Ref Expression
sspph.h
Assertion
Ref Expression
sspph

Proof of Theorem sspph
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 phnv 26431 . . 3
2 sspph.h . . . 4
32sspnv 26341 . . 3
41, 3sylan 473 . 2
5 eqid 2420 . . . . . . . . . 10
6 eqid 2420 . . . . . . . . . 10
75, 6, 2sspba 26342 . . . . . . . . 9
87sseld 3460 . . . . . . . 8
97sseld 3460 . . . . . . . 8
108, 9anim12d 565 . . . . . . 7
111, 10sylan 473 . . . . . 6
1211imp 430 . . . . 5
13 eqid 2420 . . . . . . . 8
14 eqid 2420 . . . . . . . 8
15 eqid 2420 . . . . . . . 8 CV CV
165, 13, 14, 15phpar2 26440 . . . . . . 7 CV CV CV CV
17163expb 1206 . . . . . 6 CV CV CV CV
1817adantlr 719 . . . . 5 CV CV CV CV
1912, 18syldan 472 . . . 4 CV CV CV CV
20 eqid 2420 . . . . . . . . . . . 12
216, 20nvgcl 26215 . . . . . . . . . . 11
22213expb 1206 . . . . . . . . . 10
233, 22sylan 473 . . . . . . . . 9
24 eqid 2420 . . . . . . . . . . 11 CV CV
256, 15, 24, 2sspnval 26352 . . . . . . . . . 10 CV CV
26253expa 1205 . . . . . . . . 9 CV CV
2723, 26syldan 472 . . . . . . . 8 CV CV
2827oveq1d 6312 . . . . . . 7 CV CV
296, 13, 20, 2sspgval 26344 . . . . . . . . 9
3029fveq2d 5877 . . . . . . . 8 CV CV
3130oveq1d 6312 . . . . . . 7 CV CV
3228, 31eqtrd 2461 . . . . . 6 CV CV
33 eqid 2420 . . . . . . . . . . . 12
346, 33nvmcl 26244 . . . . . . . . . . 11
35343expb 1206 . . . . . . . . . 10
363, 35sylan 473 . . . . . . . . 9
376, 15, 24, 2sspnval 26352 . . . . . . . . . 10 CV CV
38373expa 1205 . . . . . . . . 9 CV CV
3936, 38syldan 472 . . . . . . . 8 CV CV
406, 14, 33, 2sspmval 26348 . . . . . . . . 9
4140fveq2d 5877 . . . . . . . 8 CV CV
4239, 41eqtrd 2461 . . . . . . 7 CV CV
4342oveq1d 6312 . . . . . 6 CV CV
4432, 43oveq12d 6315 . . . . 5 CV CV CV CV
451, 44sylanl1 654 . . . 4 CV CV CV CV
466, 15, 24, 2sspnval 26352 . . . . . . . . . 10 CV CV
47463expa 1205 . . . . . . . . 9 CV CV
4847adantrr 721 . . . . . . . 8 CV CV
4948oveq1d 6312 . . . . . . 7 CV CV
506, 15, 24, 2sspnval 26352 . . . . . . . . . 10 CV CV
51503expa 1205 . . . . . . . . 9 CV CV
5251adantrl 720 . . . . . . . 8 CV CV
5352oveq1d 6312 . . . . . . 7 CV CV
5449, 53oveq12d 6315 . . . . . 6 CV CV CV CV
551, 54sylanl1 654 . . . . 5 CV CV CV CV
5655oveq2d 6313 . . . 4 CV CV CV CV
5719, 45, 563eqtr4d 2471 . . 3 CV CV CV CV
5857ralrimivva 2844 . 2 CV CV CV CV
596, 20, 33, 24isph 26439 . 2 CV CV CV CV
604, 58, 59sylanbrc 668 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1867  wral 2773  cfv 5593  (class class class)co 6297   caddc 9538   cmul 9540  c2 10655  cexp 12265  cnv 26179  cpv 26180  cba 26181  cnsb 26184  CVcnmcv 26185  css 26336  ccphlo 26429 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-po 4767  df-so 4768  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-1st 6799  df-2nd 6800  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9673  df-mnf 9674  df-ltxr 9676  df-sub 9858  df-neg 9859  df-grpo 25895  df-gid 25896  df-ginv 25897  df-gdiv 25898  df-ablo 25986  df-vc 26141  df-nv 26187  df-va 26190  df-ba 26191  df-sm 26192  df-0v 26193  df-vs 26194  df-nmcv 26195  df-ssp 26337  df-ph 26430 This theorem is referenced by:  ssphl  26545  hhssph  26901
 Copyright terms: Public domain W3C validator