Metamath Proof Explorer

Theorem ipval

Description: Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is G , the scalar product is S , the norm is N , and the set of vectors is X . Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
dipfval.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
dipfval.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
dipfval.6 โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
dipfval.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
Assertion ipval ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( 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 1 2 3 4 5 dipfval โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘ƒ = ( ๐‘ฅ โˆˆ ๐‘‹ , ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) ) )
7 6 oveqd โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ๐ด ( ๐‘ฅ โˆˆ ๐‘‹ , ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) ) ๐ต ) )
8 fvoveq1 โŠข ( ๐‘ฅ = ๐ด โ†’ ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) = ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) )
9 8 oveq1d โŠข ( ๐‘ฅ = ๐ด โ†’ ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) = ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) )
10 9 oveq2d โŠข ( ๐‘ฅ = ๐ด โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) )
11 10 sumeq2sdv โŠข ( ๐‘ฅ = ๐ด โ†’ ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) )
12 11 oveq1d โŠข ( ๐‘ฅ = ๐ด โ†’ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) )
13 oveq2 โŠข ( ๐‘ฆ = ๐ต โ†’ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) = ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) )
14 13 oveq2d โŠข ( ๐‘ฆ = ๐ต โ†’ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) = ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) )
15 14 fveq2d โŠข ( ๐‘ฆ = ๐ต โ†’ ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) = ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) )
16 15 oveq1d โŠข ( ๐‘ฆ = ๐ต โ†’ ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) = ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) )
17 16 oveq2d โŠข ( ๐‘ฆ = ๐ต โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) )
18 17 sumeq2sdv โŠข ( ๐‘ฆ = ๐ต โ†’ ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) )
19 18 oveq1d โŠข ( ๐‘ฆ = ๐ต โ†’ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) / 4 ) )
20 eqid โŠข ( ๐‘ฅ โˆˆ ๐‘‹ , ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ , ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) )
21 ovex โŠข ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) / 4 ) โˆˆ V
22 12 19 20 21 ovmpo โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ( ๐‘ฅ โˆˆ ๐‘‹ , ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐‘ฅ ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐‘ฆ ) ) ) โ†‘ 2 ) ) / 4 ) ) ๐ต ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) / 4 ) )
23 7 22 sylan9eq โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) / 4 ) )
24 23 3impb โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐‘ƒ ๐ต ) = ( ฮฃ ๐‘˜ โˆˆ ( 1 ... 4 ) ( ( i โ†‘ ๐‘˜ ) ยท ( ( ๐‘ โ€˜ ( ๐ด ๐บ ( ( i โ†‘ ๐‘˜ ) ๐‘† ๐ต ) ) ) โ†‘ 2 ) ) / 4 ) )