Metamath Proof Explorer

Theorem ipval3

Description: Expansion of the inner product value ipval . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
dipfval.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
dipfval.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
dipfval.6 โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
dipfval.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
ipval3.3 โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
Assertion ipval3 ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 dipfval.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 dipfval.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 dipfval.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 dipfval.6 โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
5 dipfval.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
6 ipval3.3 โŠข ๐‘€ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
7 1 2 3 4 5 ipval2 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )
8 1 2 3 6 nvmval โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘€ ๐ต ) = ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) )
9 8 fveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) = ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) )
10 9 oveq1d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) = ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โ†‘ 2 ) )
11 10 oveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) = ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) )
12 ax-icn โŠข i โˆˆ โ„‚
13 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง i โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( i ๐‘† ๐ต ) โˆˆ ๐‘‹ )
14 12 13 mp3an2 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( i ๐‘† ๐ต ) โˆˆ ๐‘‹ )
15 14 3adant2 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( i ๐‘† ๐ต ) โˆˆ ๐‘‹ )
16 1 2 3 6 nvmval โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ( i ๐‘† ๐ต ) โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) = ( ๐ด ๐บ ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) ) )
17 15 16 syld3an3 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) = ( ๐ด ๐บ ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) ) )
18 neg1cn โŠข - 1 โˆˆ โ„‚
19 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 โˆˆ โ„‚ โˆง i โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ( - 1 ยท i ) ๐‘† ๐ต ) = ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) )
20 18 19 mp3anr1 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( i โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ( - 1 ยท i ) ๐‘† ๐ต ) = ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) )
21 12 20 mpanr1 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( - 1 ยท i ) ๐‘† ๐ต ) = ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) )
22 12 mulm1i โŠข ( - 1 ยท i ) = - i
23 22 oveq1i โŠข ( ( - 1 ยท i ) ๐‘† ๐ต ) = ( - i ๐‘† ๐ต )
24 21 23 eqtr3di โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) = ( - i ๐‘† ๐ต ) )
25 24 3adant2 โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) = ( - i ๐‘† ๐ต ) )
26 25 oveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ( - 1 ๐‘† ( i ๐‘† ๐ต ) ) ) = ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) )
27 17 26 eqtrd โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) = ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) )
28 27 fveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) = ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) )
29 28 oveq1d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) = ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) )
30 29 oveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) = ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) )
31 30 oveq2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) = ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) )
32 11 31 oveq12d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) = ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) )
33 32 oveq1d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) = ( ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( - i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )
34 7 33 eqtr4d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ( ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ๐ต ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ๐ต ) ) โ†‘ 2 ) ) + ( i ยท ( ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) โˆ’ ( ( ๐‘ โ€˜ ( ๐ด ๐‘€ ( i ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) ) ) / 4 ) )