MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspimsval Structured version   Visualization version   GIF version

Theorem sspimsval 29145
Description: The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
Hypotheses
Ref Expression
sspims.y π‘Œ = (BaseSetβ€˜π‘Š)
sspims.d 𝐷 = (IndMetβ€˜π‘ˆ)
sspims.c 𝐢 = (IndMetβ€˜π‘Š)
sspims.h 𝐻 = (SubSpβ€˜π‘ˆ)
Assertion
Ref Expression
sspimsval (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴𝐢𝐡) = (𝐴𝐷𝐡))

Proof of Theorem sspimsval
StepHypRef Expression
1 sspims.h . . . . . 6 𝐻 = (SubSpβ€˜π‘ˆ)
21sspnv 29133 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) β†’ π‘Š ∈ NrmCVec)
3 sspims.y . . . . . . 7 π‘Œ = (BaseSetβ€˜π‘Š)
4 eqid 2736 . . . . . . 7 ( βˆ’π‘£ β€˜π‘Š) = ( βˆ’π‘£ β€˜π‘Š)
53, 4nvmcl 29053 . . . . . 6 ((π‘Š ∈ NrmCVec ∧ 𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ) β†’ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) ∈ π‘Œ)
653expb 1120 . . . . 5 ((π‘Š ∈ NrmCVec ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) ∈ π‘Œ)
72, 6sylan 581 . . . 4 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) ∈ π‘Œ)
8 eqid 2736 . . . . . 6 (normCVβ€˜π‘ˆ) = (normCVβ€˜π‘ˆ)
9 eqid 2736 . . . . . 6 (normCVβ€˜π‘Š) = (normCVβ€˜π‘Š)
103, 8, 9, 1sspnval 29144 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻 ∧ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) ∈ π‘Œ) β†’ ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
11103expa 1118 . . . 4 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) ∈ π‘Œ) β†’ ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
127, 11syldan 592 . . 3 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
13 eqid 2736 . . . . 5 ( βˆ’π‘£ β€˜π‘ˆ) = ( βˆ’π‘£ β€˜π‘ˆ)
143, 13, 4, 1sspmval 29140 . . . 4 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴( βˆ’π‘£ β€˜π‘Š)𝐡) = (𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡))
1514fveq2d 6808 . . 3 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
1612, 15eqtrd 2776 . 2 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
17 sspims.c . . . . 5 𝐢 = (IndMetβ€˜π‘Š)
183, 4, 9, 17imsdval 29093 . . . 4 ((π‘Š ∈ NrmCVec ∧ 𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ) β†’ (𝐴𝐢𝐡) = ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
19183expb 1120 . . 3 ((π‘Š ∈ NrmCVec ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴𝐢𝐡) = ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
202, 19sylan 581 . 2 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴𝐢𝐡) = ((normCVβ€˜π‘Š)β€˜(𝐴( βˆ’π‘£ β€˜π‘Š)𝐡)))
21 eqid 2736 . . . . . . 7 (BaseSetβ€˜π‘ˆ) = (BaseSetβ€˜π‘ˆ)
2221, 3, 1sspba 29134 . . . . . 6 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) β†’ π‘Œ βŠ† (BaseSetβ€˜π‘ˆ))
2322sseld 3925 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) β†’ (𝐴 ∈ π‘Œ β†’ 𝐴 ∈ (BaseSetβ€˜π‘ˆ)))
2422sseld 3925 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) β†’ (𝐡 ∈ π‘Œ β†’ 𝐡 ∈ (BaseSetβ€˜π‘ˆ)))
2523, 24anim12d 610 . . . 4 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) β†’ ((𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ) β†’ (𝐴 ∈ (BaseSetβ€˜π‘ˆ) ∧ 𝐡 ∈ (BaseSetβ€˜π‘ˆ))))
2625imp 408 . . 3 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴 ∈ (BaseSetβ€˜π‘ˆ) ∧ 𝐡 ∈ (BaseSetβ€˜π‘ˆ)))
27 sspims.d . . . . . 6 𝐷 = (IndMetβ€˜π‘ˆ)
2821, 13, 8, 27imsdval 29093 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ 𝐴 ∈ (BaseSetβ€˜π‘ˆ) ∧ 𝐡 ∈ (BaseSetβ€˜π‘ˆ)) β†’ (𝐴𝐷𝐡) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
29283expb 1120 . . . 4 ((π‘ˆ ∈ NrmCVec ∧ (𝐴 ∈ (BaseSetβ€˜π‘ˆ) ∧ 𝐡 ∈ (BaseSetβ€˜π‘ˆ))) β†’ (𝐴𝐷𝐡) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
3029adantlr 713 . . 3 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ (BaseSetβ€˜π‘ˆ) ∧ 𝐡 ∈ (BaseSetβ€˜π‘ˆ))) β†’ (𝐴𝐷𝐡) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
3126, 30syldan 592 . 2 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴𝐷𝐡) = ((normCVβ€˜π‘ˆ)β€˜(𝐴( βˆ’π‘£ β€˜π‘ˆ)𝐡)))
3216, 20, 313eqtr4d 2786 1 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ 𝐻) ∧ (𝐴 ∈ π‘Œ ∧ 𝐡 ∈ π‘Œ)) β†’ (𝐴𝐢𝐡) = (𝐴𝐷𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  β€˜cfv 6458  (class class class)co 7307  NrmCVeccnv 28991  BaseSetcba 28993   βˆ’π‘£ cnsb 28996  normCVcnmcv 28997  IndMetcims 28998  SubSpcss 29128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-1st 7863  df-2nd 7864  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-ltxr 11060  df-sub 11253  df-neg 11254  df-grpo 28900  df-gid 28901  df-ginv 28902  df-gdiv 28903  df-ablo 28952  df-vc 28966  df-nv 28999  df-va 29002  df-ba 29003  df-sm 29004  df-0v 29005  df-vs 29006  df-nmcv 29007  df-ims 29008  df-ssp 29129
This theorem is referenced by:  sspims  29146
  Copyright terms: Public domain W3C validator