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

Theorem hvsubid 21599
Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
hvsubid  |-  ( A  e.  ~H  ->  ( A  -h  A )  =  0h )

Proof of Theorem hvsubid
StepHypRef Expression
1 ax-hvmulid 21580 . . . . 5  |-  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
21oveq1d 5836 . . . 4  |-  ( A  e.  ~H  ->  (
( 1  .h  A
)  +h  ( -u
1  .h  A ) )  =  ( A  +h  ( -u 1  .h  A ) ) )
3 ax-1cn 8792 . . . . 5  |-  1  e.  CC
4 neg1cn 9810 . . . . 5  |-  -u 1  e.  CC
5 ax-hvdistr2 21583 . . . . 5  |-  ( ( 1  e.  CC  /\  -u 1  e.  CC  /\  A  e.  ~H )  ->  ( ( 1  + 
-u 1 )  .h  A )  =  ( ( 1  .h  A
)  +h  ( -u
1  .h  A ) ) )
63, 4, 5mp3an12 1269 . . . 4  |-  ( A  e.  ~H  ->  (
( 1  +  -u
1 )  .h  A
)  =  ( ( 1  .h  A )  +h  ( -u 1  .h  A ) ) )
7 hvsubval 21590 . . . . 5  |-  ( ( A  e.  ~H  /\  A  e.  ~H )  ->  ( A  -h  A
)  =  ( A  +h  ( -u 1  .h  A ) ) )
87anidms 628 . . . 4  |-  ( A  e.  ~H  ->  ( A  -h  A )  =  ( A  +h  ( -u 1  .h  A ) ) )
92, 6, 83eqtr4rd 2329 . . 3  |-  ( A  e.  ~H  ->  ( A  -h  A )  =  ( ( 1  + 
-u 1 )  .h  A ) )
103negidi 9112 . . . 4  |-  ( 1  +  -u 1 )  =  0
1110oveq1i 5831 . . 3  |-  ( ( 1  +  -u 1
)  .h  A )  =  ( 0  .h  A )
129, 11syl6eq 2334 . 2  |-  ( A  e.  ~H  ->  ( A  -h  A )  =  ( 0  .h  A
) )
13 ax-hvmul0 21584 . 2  |-  ( A  e.  ~H  ->  (
0  .h  A )  =  0h )
1412, 13eqtrd 2318 1  |-  ( A  e.  ~H  ->  ( A  -h  A )  =  0h )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1625    e. wcel 1687  (class class class)co 5821   CCcc 8732   0cc0 8734   1c1 8735    + caddc 8737   -ucneg 9035   ~Hchil 21493    +h cva 21494    .h csm 21495   0hc0v 21498    -h cmv 21499
This theorem is referenced by:  hvnegid  21600  hvsubeq0i  21636  hvaddsub4  21651  norm3difi  21720  5oalem1  22227  5oalem2  22228  5oalem3  22229  5oalem5  22231  3oalem2  22236  pjsslem  22252  ho0val  22324  lnop0  22540  0cnop  22553  pjclem4  22773  pj3si  22781
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810  ax-hvmulid 21580  ax-hvdistr2 21583  ax-hvmul0 21584
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-reu 2553  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-mpt 4082  df-id 4310  df-po 4315  df-so 4316  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-iota 6254  df-riota 6301  df-er 6657  df-en 6861  df-dom 6862  df-sdom 6863  df-pnf 8866  df-mnf 8867  df-ltxr 8869  df-sub 9036  df-neg 9037  df-hvsub 21545
  Copyright terms: Public domain W3C validator