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 | |
|
cphipcj.v | |
||
cphass.f | |
||
cphass.k | |
||
cphass.s | |
||
Assertion | cphassr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cphipcj.h | |
|
2 | cphipcj.v | |
|
3 | cphass.f | |
|
4 | cphass.k | |
|
5 | cphass.s | |
|
6 | cphclm | |
|
7 | 6 | adantr | |
8 | 3 | clmmul | |
9 | 7 8 | syl | |
10 | eqidd | |
|
11 | 3 | clmcj | |
12 | 7 11 | syl | |
13 | 12 | fveq1d | |
14 | 9 10 13 | oveq123d | |
15 | 3 4 | clmsscn | |
16 | 7 15 | syl | |
17 | simpr1 | |
|
18 | 16 17 | sseldd | |
19 | 18 | cjcld | |
20 | 2 1 | cphipcl | |
21 | 20 | 3adant3r1 | |
22 | 19 21 | mulcomd | |
23 | cphphl | |
|
24 | 3anrot | |
|
25 | 24 | biimpi | |
26 | eqid | |
|
27 | eqid | |
|
28 | 3 1 2 4 5 26 27 | ipassr | |
29 | 23 25 28 | syl2an | |
30 | 14 22 29 | 3eqtr4rd | |