Metamath Proof Explorer


Theorem cphassr

Description: "Associative" law for second argument of inner product (compare cphass ). See ipassr , his52 . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h โŠข,ห™=โ‹…๐‘–โกW
cphipcj.v โŠขV=BaseW
cphass.f โŠขF=ScalarโกW
cphass.k โŠขK=BaseF
cphass.s โŠขยทห™=โ‹…W
Assertion cphassr โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™Aยทห™C=Aโ€พโขB,ห™C

Proof

Step Hyp Ref Expression
1 cphipcj.h โŠข,ห™=โ‹…๐‘–โกW
2 cphipcj.v โŠขV=BaseW
3 cphass.f โŠขF=ScalarโกW
4 cphass.k โŠขK=BaseF
5 cphass.s โŠขยทห™=โ‹…W
6 cphclm โŠขWโˆˆCPreHilโ†’WโˆˆCMod
7 6 adantr โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’WโˆˆCMod
8 3 clmmul โŠขWโˆˆCModโ†’ร—=โ‹…F
9 7 8 syl โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’ร—=โ‹…F
10 eqidd โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™C=B,ห™C
11 3 clmcj โŠขWโˆˆCModโ†’*=*F
12 7 11 syl โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’*=*F
13 12 fveq1d โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’Aโ€พ=A*F
14 9 10 13 oveq123d โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™CโขAโ€พ=B,ห™Cโ‹…FA*F
15 3 4 clmsscn โŠขWโˆˆCModโ†’KโІโ„‚
16 7 15 syl โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’KโІโ„‚
17 simpr1 โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’AโˆˆK
18 16 17 sseldd โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’Aโˆˆโ„‚
19 18 cjcld โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’Aโ€พโˆˆโ„‚
20 2 1 cphipcl โŠขWโˆˆCPreHilโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™Cโˆˆโ„‚
21 20 3adant3r1 โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™Cโˆˆโ„‚
22 19 21 mulcomd โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’Aโ€พโขB,ห™C=B,ห™CโขAโ€พ
23 cphphl โŠขWโˆˆCPreHilโ†’WโˆˆPreHil
24 3anrot โŠขAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†”BโˆˆVโˆงCโˆˆVโˆงAโˆˆK
25 24 biimpi โŠขAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’BโˆˆVโˆงCโˆˆVโˆงAโˆˆK
26 eqid โŠขโ‹…F=โ‹…F
27 eqid โŠข*F=*F
28 3 1 2 4 5 26 27 ipassr โŠขWโˆˆPreHilโˆงBโˆˆVโˆงCโˆˆVโˆงAโˆˆKโ†’B,ห™Aยทห™C=B,ห™Cโ‹…FA*F
29 23 25 28 syl2an โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™Aยทห™C=B,ห™Cโ‹…FA*F
30 14 22 29 3eqtr4rd โŠขWโˆˆCPreHilโˆงAโˆˆKโˆงBโˆˆVโˆงCโˆˆVโ†’B,ห™Aยทห™C=Aโ€พโขB,ห™C