HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  normlem9 Structured version   Visualization version   GIF version

Theorem normlem9 28899
Description: Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
normlem8.1 𝐴 ∈ ℋ
normlem8.2 𝐵 ∈ ℋ
normlem8.3 𝐶 ∈ ℋ
normlem8.4 𝐷 ∈ ℋ
Assertion
Ref Expression
normlem9 ((𝐴 𝐵) ·ih (𝐶 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))

Proof of Theorem normlem9
StepHypRef Expression
1 normlem8.1 . . . 4 𝐴 ∈ ℋ
2 normlem8.2 . . . 4 𝐵 ∈ ℋ
31, 2hvsubvali 28801 . . 3 (𝐴 𝐵) = (𝐴 + (-1 · 𝐵))
4 normlem8.3 . . . 4 𝐶 ∈ ℋ
5 normlem8.4 . . . 4 𝐷 ∈ ℋ
64, 5hvsubvali 28801 . . 3 (𝐶 𝐷) = (𝐶 + (-1 · 𝐷))
73, 6oveq12i 7158 . 2 ((𝐴 𝐵) ·ih (𝐶 𝐷)) = ((𝐴 + (-1 · 𝐵)) ·ih (𝐶 + (-1 · 𝐷)))
8 neg1cn 11746 . . . 4 -1 ∈ ℂ
98, 2hvmulcli 28795 . . 3 (-1 · 𝐵) ∈ ℋ
108, 5hvmulcli 28795 . . 3 (-1 · 𝐷) ∈ ℋ
111, 9, 4, 10normlem8 28898 . 2 ((𝐴 + (-1 · 𝐵)) ·ih (𝐶 + (-1 · 𝐷))) = (((𝐴 ·ih 𝐶) + ((-1 · 𝐵) ·ih (-1 · 𝐷))) + ((𝐴 ·ih (-1 · 𝐷)) + ((-1 · 𝐵) ·ih 𝐶)))
12 ax-his3 28865 . . . . . . 7 ((-1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ (-1 · 𝐷) ∈ ℋ) → ((-1 · 𝐵) ·ih (-1 · 𝐷)) = (-1 · (𝐵 ·ih (-1 · 𝐷))))
138, 2, 10, 12mp3an 1458 . . . . . 6 ((-1 · 𝐵) ·ih (-1 · 𝐷)) = (-1 · (𝐵 ·ih (-1 · 𝐷)))
14 his5 28867 . . . . . . . 8 ((-1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐵 ·ih (-1 · 𝐷)) = ((∗‘-1) · (𝐵 ·ih 𝐷)))
158, 2, 5, 14mp3an 1458 . . . . . . 7 (𝐵 ·ih (-1 · 𝐷)) = ((∗‘-1) · (𝐵 ·ih 𝐷))
1615oveq2i 7157 . . . . . 6 (-1 · (𝐵 ·ih (-1 · 𝐷))) = (-1 · ((∗‘-1) · (𝐵 ·ih 𝐷)))
17 neg1rr 11747 . . . . . . . . . . 11 -1 ∈ ℝ
18 cjre 14496 . . . . . . . . . . 11 (-1 ∈ ℝ → (∗‘-1) = -1)
1917, 18ax-mp 5 . . . . . . . . . 10 (∗‘-1) = -1
2019oveq2i 7157 . . . . . . . . 9 (-1 · (∗‘-1)) = (-1 · -1)
21 ax-1cn 10589 . . . . . . . . . 10 1 ∈ ℂ
2221, 21mul2negi 11082 . . . . . . . . 9 (-1 · -1) = (1 · 1)
2321mulid2i 10640 . . . . . . . . 9 (1 · 1) = 1
2420, 22, 233eqtri 2851 . . . . . . . 8 (-1 · (∗‘-1)) = 1
2524oveq1i 7156 . . . . . . 7 ((-1 · (∗‘-1)) · (𝐵 ·ih 𝐷)) = (1 · (𝐵 ·ih 𝐷))
268cjcli 14526 . . . . . . . 8 (∗‘-1) ∈ ℂ
272, 5hicli 28862 . . . . . . . 8 (𝐵 ·ih 𝐷) ∈ ℂ
288, 26, 27mulassi 10646 . . . . . . 7 ((-1 · (∗‘-1)) · (𝐵 ·ih 𝐷)) = (-1 · ((∗‘-1) · (𝐵 ·ih 𝐷)))
2927mulid2i 10640 . . . . . . 7 (1 · (𝐵 ·ih 𝐷)) = (𝐵 ·ih 𝐷)
3025, 28, 293eqtr3i 2855 . . . . . 6 (-1 · ((∗‘-1) · (𝐵 ·ih 𝐷))) = (𝐵 ·ih 𝐷)
3113, 16, 303eqtri 2851 . . . . 5 ((-1 · 𝐵) ·ih (-1 · 𝐷)) = (𝐵 ·ih 𝐷)
3231oveq2i 7157 . . . 4 ((𝐴 ·ih 𝐶) + ((-1 · 𝐵) ·ih (-1 · 𝐷))) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷))
33 his5 28867 . . . . . . . 8 ((-1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐷 ∈ ℋ) → (𝐴 ·ih (-1 · 𝐷)) = ((∗‘-1) · (𝐴 ·ih 𝐷)))
348, 1, 5, 33mp3an 1458 . . . . . . 7 (𝐴 ·ih (-1 · 𝐷)) = ((∗‘-1) · (𝐴 ·ih 𝐷))
3519oveq1i 7156 . . . . . . 7 ((∗‘-1) · (𝐴 ·ih 𝐷)) = (-1 · (𝐴 ·ih 𝐷))
361, 5hicli 28862 . . . . . . . 8 (𝐴 ·ih 𝐷) ∈ ℂ
3736mulm1i 11079 . . . . . . 7 (-1 · (𝐴 ·ih 𝐷)) = -(𝐴 ·ih 𝐷)
3834, 35, 373eqtri 2851 . . . . . 6 (𝐴 ·ih (-1 · 𝐷)) = -(𝐴 ·ih 𝐷)
39 ax-his3 28865 . . . . . . . 8 ((-1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((-1 · 𝐵) ·ih 𝐶) = (-1 · (𝐵 ·ih 𝐶)))
408, 2, 4, 39mp3an 1458 . . . . . . 7 ((-1 · 𝐵) ·ih 𝐶) = (-1 · (𝐵 ·ih 𝐶))
412, 4hicli 28862 . . . . . . . 8 (𝐵 ·ih 𝐶) ∈ ℂ
4241mulm1i 11079 . . . . . . 7 (-1 · (𝐵 ·ih 𝐶)) = -(𝐵 ·ih 𝐶)
4340, 42eqtri 2847 . . . . . 6 ((-1 · 𝐵) ·ih 𝐶) = -(𝐵 ·ih 𝐶)
4438, 43oveq12i 7158 . . . . 5 ((𝐴 ·ih (-1 · 𝐷)) + ((-1 · 𝐵) ·ih 𝐶)) = (-(𝐴 ·ih 𝐷) + -(𝐵 ·ih 𝐶))
4536, 41negdii 10964 . . . . 5 -((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)) = (-(𝐴 ·ih 𝐷) + -(𝐵 ·ih 𝐶))
4644, 45eqtr4i 2850 . . . 4 ((𝐴 ·ih (-1 · 𝐷)) + ((-1 · 𝐵) ·ih 𝐶)) = -((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))
4732, 46oveq12i 7158 . . 3 (((𝐴 ·ih 𝐶) + ((-1 · 𝐵) ·ih (-1 · 𝐷))) + ((𝐴 ·ih (-1 · 𝐷)) + ((-1 · 𝐵) ·ih 𝐶))) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + -((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
481, 4hicli 28862 . . . . 5 (𝐴 ·ih 𝐶) ∈ ℂ
4948, 27addcli 10641 . . . 4 ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) ∈ ℂ
5036, 41addcli 10641 . . . 4 ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)) ∈ ℂ
5149, 50negsubi 10958 . . 3 (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + -((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
5247, 51eqtri 2847 . 2 (((𝐴 ·ih 𝐶) + ((-1 · 𝐵) ·ih (-1 · 𝐷))) + ((𝐴 ·ih (-1 · 𝐷)) + ((-1 · 𝐵) ·ih 𝐶))) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
537, 11, 523eqtri 2851 1 ((𝐴 𝐵) ·ih (𝐶 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  cfv 6344  (class class class)co 7146  cc 10529  cr 10530  1c1 10532   + caddc 10534   · cmul 10536  cmin 10864  -cneg 10865  ccj 14453  chba 28700   + cva 28701   · csm 28702   ·ih csp 28703   cmv 28706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-hfvadd 28781  ax-hfvmul 28786  ax-hfi 28860  ax-his1 28863  ax-his2 28864  ax-his3 28865
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-po 5462  df-so 5463  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-2 11695  df-cj 14456  df-re 14457  df-im 14458  df-hvsub 28752
This theorem is referenced by:  bcseqi  28901  normlem9at  28902  normpari  28935  polid2i  28938
  Copyright terms: Public domain W3C validator