# Metamath Proof Explorer

## Theorem 4ipval2

Description: Four times the inner product value ipval3 , useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
dipfval.2 ${⊢}{G}={+}_{v}\left({U}\right)$
dipfval.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
dipfval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
dipfval.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
Assertion 4ipval2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 4\left({A}{P}{B}\right)={{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)$

### Proof

Step Hyp Ref Expression
1 dipfval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 dipfval.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 dipfval.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
4 dipfval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
5 dipfval.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
6 1 2 3 4 5 ipval2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{P}{B}=\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}$
7 6 oveq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 4\left({A}{P}{B}\right)=4\left(\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}\right)$
8 simp1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {U}\in \mathrm{NrmCVec}$
9 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
10 1 4 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}{B}\in {X}\right)\to {N}\left({A}{G}{B}\right)\in ℝ$
11 8 9 10 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}{B}\right)\in ℝ$
12 11 recnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}{B}\right)\in ℂ$
13 12 sqcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}{B}\right)}^{2}\in ℂ$
14 neg1cn ${⊢}-1\in ℂ$
15 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -1\in ℂ\wedge {B}\in {X}\right)\to -1{S}{B}\in {X}$
16 14 15 mp3an2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to -1{S}{B}\in {X}$
17 16 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to -1{S}{B}\in {X}$
18 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge -1{S}{B}\in {X}\right)\to {A}{G}\left(-1{S}{B}\right)\in {X}$
19 17 18 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}\left(-1{S}{B}\right)\in {X}$
20 1 4 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}\left(-1{S}{B}\right)\in {X}\right)\to {N}\left({A}{G}\left(-1{S}{B}\right)\right)\in ℝ$
21 8 19 20 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(-1{S}{B}\right)\right)\in ℝ$
22 21 recnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(-1{S}{B}\right)\right)\in ℂ$
23 22 sqcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}\in ℂ$
24 13 23 subcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}\in ℂ$
25 ax-icn ${⊢}\mathrm{i}\in ℂ$
26 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \mathrm{i}\in ℂ\wedge {B}\in {X}\right)\to \mathrm{i}{S}{B}\in {X}$
27 25 26 mp3an2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to \mathrm{i}{S}{B}\in {X}$
28 27 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \mathrm{i}{S}{B}\in {X}$
29 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge \mathrm{i}{S}{B}\in {X}\right)\to {A}{G}\left(\mathrm{i}{S}{B}\right)\in {X}$
30 28 29 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}\left(\mathrm{i}{S}{B}\right)\in {X}$
31 1 4 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}\left(\mathrm{i}{S}{B}\right)\in {X}\right)\to {N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)\in ℝ$
32 8 30 31 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)\in ℝ$
33 32 recnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)\in ℂ$
34 33 sqcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}\in ℂ$
35 negicn ${⊢}-\mathrm{i}\in ℂ$
36 1 3 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -\mathrm{i}\in ℂ\wedge {B}\in {X}\right)\to \left(-\mathrm{i}\right){S}{B}\in {X}$
37 35 36 mp3an2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to \left(-\mathrm{i}\right){S}{B}\in {X}$
38 37 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left(-\mathrm{i}\right){S}{B}\in {X}$
39 1 2 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge \left(-\mathrm{i}\right){S}{B}\in {X}\right)\to {A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\in {X}$
40 38 39 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\in {X}$
41 1 4 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\in {X}\right)\to {N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)\in ℝ$
42 8 40 41 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)\in ℝ$
43 42 recnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)\in ℂ$
44 43 sqcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\in ℂ$
45 34 44 subcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\in ℂ$
46 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge {{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\in ℂ\right)\to \mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)\in ℂ$
47 25 45 46 sylancr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)\in ℂ$
48 24 47 addcld ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)\in ℂ$
49 4cn ${⊢}4\in ℂ$
50 4ne0 ${⊢}4\ne 0$
51 divcan2 ${⊢}\left({{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)\in ℂ\wedge 4\in ℂ\wedge 4\ne 0\right)\to 4\left(\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}\right)={{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)$
52 49 50 51 mp3an23 ${⊢}{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)\in ℂ\to 4\left(\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}\right)={{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)$
53 48 52 syl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 4\left(\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}\right)={{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)$
54 7 53 eqtrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 4\left({A}{P}{B}\right)={{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)$