Metamath Proof Explorer

Theorem ipasslem11

Description: Lemma for ipassi . Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 
|- X = ( BaseSet ` U )
ip1i.2 
|- G = ( +v ` U )
ip1i.4 
|- S = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ipasslem11.a 
|- A e. X
ipasslem11.b 
|- B e. X
Assertion ipasslem11 
|- ( C e. CC -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 
 |-  X = ( BaseSet ` U )
2 ip1i.2 
 |-  G = ( +v ` U )
3 ip1i.4 
 |-  S = ( .sOLD ` U )
4 ip1i.7 
 |-  P = ( .iOLD ` U )
5 ip1i.9 
 |-  U e. CPreHilOLD
6 ipasslem11.a 
 |-  A e. X
7 ipasslem11.b 
 |-  B e. X
8 cnre 
 |-  ( C e. CC -> E. x e. RR E. y e. RR C = ( x + ( _i x. y ) ) )
9 ax-icn 
 |-  _i e. CC
10 recn 
 |-  ( y e. RR -> y e. CC )
11 mulcom 
 |-  ( ( _i e. CC /\ y e. CC ) -> ( _i x. y ) = ( y x. _i ) )
12 9 10 11 sylancr 
 |-  ( y e. RR -> ( _i x. y ) = ( y x. _i ) )
13 12 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) = ( y x. _i ) )
14 13 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) = ( x + ( y x. _i ) ) )
15 14 eqeq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( C = ( x + ( _i x. y ) ) <-> C = ( x + ( y x. _i ) ) ) )
16 recn 
 |-  ( x e. RR -> x e. CC )
17 5 phnvi 
 |-  U e. NrmCVec
18 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ x e. CC /\ A e. X ) -> ( x S A ) e. X )
19 17 6 18 mp3an13 
 |-  ( x e. CC -> ( x S A ) e. X )
20 16 19 syl 
 |-  ( x e. RR -> ( x S A ) e. X )
21 mulcl 
 |-  ( ( y e. CC /\ _i e. CC ) -> ( y x. _i ) e. CC )
22 10 9 21 sylancl 
 |-  ( y e. RR -> ( y x. _i ) e. CC )
23 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ ( y x. _i ) e. CC /\ A e. X ) -> ( ( y x. _i ) S A ) e. X )
24 17 6 23 mp3an13 
 |-  ( ( y x. _i ) e. CC -> ( ( y x. _i ) S A ) e. X )
25 22 24 syl 
 |-  ( y e. RR -> ( ( y x. _i ) S A ) e. X )
26 1 2 3 4 5 ipdiri 
 |-  ( ( ( x S A ) e. X /\ ( ( y x. _i ) S A ) e. X /\ B e. X ) -> ( ( ( x S A ) G ( ( y x. _i ) S A ) ) P B ) = ( ( ( x S A ) P B ) + ( ( ( y x. _i ) S A ) P B ) ) )
27 7 26 mp3an3 
 |-  ( ( ( x S A ) e. X /\ ( ( y x. _i ) S A ) e. X ) -> ( ( ( x S A ) G ( ( y x. _i ) S A ) ) P B ) = ( ( ( x S A ) P B ) + ( ( ( y x. _i ) S A ) P B ) ) )
28 20 25 27 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x S A ) G ( ( y x. _i ) S A ) ) P B ) = ( ( ( x S A ) P B ) + ( ( ( y x. _i ) S A ) P B ) ) )
29 1 2 3 4 5 6 7 ipasslem9 
 |-  ( x e. RR -> ( ( x S A ) P B ) = ( x x. ( A P B ) ) )
30 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ _i e. CC /\ A e. X ) -> ( _i S A ) e. X )
31 17 9 6 30 mp3an 
 |-  ( _i S A ) e. X
32 1 2 3 4 5 31 7 ipasslem9 
 |-  ( y e. RR -> ( ( y S ( _i S A ) ) P B ) = ( y x. ( ( _i S A ) P B ) ) )
33 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( y e. CC /\ _i e. CC /\ A e. X ) ) -> ( ( y x. _i ) S A ) = ( y S ( _i S A ) ) )
34 17 33 mpan 
 |-  ( ( y e. CC /\ _i e. CC /\ A e. X ) -> ( ( y x. _i ) S A ) = ( y S ( _i S A ) ) )
35 9 6 34 mp3an23 
 |-  ( y e. CC -> ( ( y x. _i ) S A ) = ( y S ( _i S A ) ) )
36 10 35 syl 
 |-  ( y e. RR -> ( ( y x. _i ) S A ) = ( y S ( _i S A ) ) )
37 36 oveq1d 
 |-  ( y e. RR -> ( ( ( y x. _i ) S A ) P B ) = ( ( y S ( _i S A ) ) P B ) )
38 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
39 17 6 7 38 mp3an 
 |-  ( A P B ) e. CC
40 mulass 
 |-  ( ( y e. CC /\ _i e. CC /\ ( A P B ) e. CC ) -> ( ( y x. _i ) x. ( A P B ) ) = ( y x. ( _i x. ( A P B ) ) ) )
41 9 39 40 mp3an23 
 |-  ( y e. CC -> ( ( y x. _i ) x. ( A P B ) ) = ( y x. ( _i x. ( A P B ) ) ) )
42 10 41 syl 
 |-  ( y e. RR -> ( ( y x. _i ) x. ( A P B ) ) = ( y x. ( _i x. ( A P B ) ) ) )
43 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
44 1 2 3 4 5 6 7 43 ipasslem10 
 |-  ( ( _i S A ) P B ) = ( _i x. ( A P B ) )
45 44 oveq2i 
 |-  ( y x. ( ( _i S A ) P B ) ) = ( y x. ( _i x. ( A P B ) ) )
46 42 45 eqtr4di 
 |-  ( y e. RR -> ( ( y x. _i ) x. ( A P B ) ) = ( y x. ( ( _i S A ) P B ) ) )
47 32 37 46 3eqtr4d 
 |-  ( y e. RR -> ( ( ( y x. _i ) S A ) P B ) = ( ( y x. _i ) x. ( A P B ) ) )
48 29 47 oveqan12d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x S A ) P B ) + ( ( ( y x. _i ) S A ) P B ) ) = ( ( x x. ( A P B ) ) + ( ( y x. _i ) x. ( A P B ) ) ) )
49 28 48 eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x S A ) G ( ( y x. _i ) S A ) ) P B ) = ( ( x x. ( A P B ) ) + ( ( y x. _i ) x. ( A P B ) ) ) )
50 1 2 3 nvdir 
 |-  ( ( U e. NrmCVec /\ ( x e. CC /\ ( y x. _i ) e. CC /\ A e. X ) ) -> ( ( x + ( y x. _i ) ) S A ) = ( ( x S A ) G ( ( y x. _i ) S A ) ) )
51 17 50 mpan 
 |-  ( ( x e. CC /\ ( y x. _i ) e. CC /\ A e. X ) -> ( ( x + ( y x. _i ) ) S A ) = ( ( x S A ) G ( ( y x. _i ) S A ) ) )
52 6 51 mp3an3 
 |-  ( ( x e. CC /\ ( y x. _i ) e. CC ) -> ( ( x + ( y x. _i ) ) S A ) = ( ( x S A ) G ( ( y x. _i ) S A ) ) )
53 16 22 52 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( y x. _i ) ) S A ) = ( ( x S A ) G ( ( y x. _i ) S A ) ) )
54 53 oveq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( y x. _i ) ) S A ) P B ) = ( ( ( x S A ) G ( ( y x. _i ) S A ) ) P B ) )
55 adddir 
 |-  ( ( x e. CC /\ ( y x. _i ) e. CC /\ ( A P B ) e. CC ) -> ( ( x + ( y x. _i ) ) x. ( A P B ) ) = ( ( x x. ( A P B ) ) + ( ( y x. _i ) x. ( A P B ) ) ) )
56 39 55 mp3an3 
 |-  ( ( x e. CC /\ ( y x. _i ) e. CC ) -> ( ( x + ( y x. _i ) ) x. ( A P B ) ) = ( ( x x. ( A P B ) ) + ( ( y x. _i ) x. ( A P B ) ) ) )
57 16 22 56 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( y x. _i ) ) x. ( A P B ) ) = ( ( x x. ( A P B ) ) + ( ( y x. _i ) x. ( A P B ) ) ) )
58 49 54 57 3eqtr4d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( y x. _i ) ) S A ) P B ) = ( ( x + ( y x. _i ) ) x. ( A P B ) ) )
59 oveq1 
 |-  ( C = ( x + ( y x. _i ) ) -> ( C S A ) = ( ( x + ( y x. _i ) ) S A ) )
60 59 oveq1d 
 |-  ( C = ( x + ( y x. _i ) ) -> ( ( C S A ) P B ) = ( ( ( x + ( y x. _i ) ) S A ) P B ) )
61 oveq1 
 |-  ( C = ( x + ( y x. _i ) ) -> ( C x. ( A P B ) ) = ( ( x + ( y x. _i ) ) x. ( A P B ) ) )
62 60 61 eqeq12d 
 |-  ( C = ( x + ( y x. _i ) ) -> ( ( ( C S A ) P B ) = ( C x. ( A P B ) ) <-> ( ( ( x + ( y x. _i ) ) S A ) P B ) = ( ( x + ( y x. _i ) ) x. ( A P B ) ) ) )
63 58 62 syl5ibrcom 
 |-  ( ( x e. RR /\ y e. RR ) -> ( C = ( x + ( y x. _i ) ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
64 15 63 sylbid 
 |-  ( ( x e. RR /\ y e. RR ) -> ( C = ( x + ( _i x. y ) ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) ) )
65 64 rexlimivv 
 |-  ( E. x e. RR E. y e. RR C = ( x + ( _i x. y ) ) -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )
66 8 65 syl 
 |-  ( C e. CC -> ( ( C S A ) P B ) = ( C x. ( A P B ) ) )