Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cph2ass Structured version   Unicode version

Theorem cph2ass 19180
 Description: Move scalar multiplication to outside of inner product. See his35 22595. (Contributed by Mario Carneiro, 17-Oct-2015.)
Hypotheses
Ref Expression
cphipcj.h
cphipcj.v
cphass.f Scalar
cphass.k
cphass.s
Assertion
Ref Expression
cph2ass

Proof of Theorem cph2ass
StepHypRef Expression
1 simp1 958 . . . 4
2 simp2r 985 . . . 4
3 simp3l 986 . . . 4
4 simp3r 987 . . . 4
5 cphipcj.h . . . . 5
6 cphipcj.v . . . . 5
7 cphass.f . . . . 5 Scalar
8 cphass.k . . . . 5
9 cphass.s . . . . 5
105, 6, 7, 8, 9cphassr 19179 . . . 4
111, 2, 3, 4, 10syl13anc 1187 . . 3
1211oveq2d 6100 . 2
13 simp2l 984 . . 3
14 cphlmod 19142 . . . . 5
15143ad2ant1 979 . . . 4
166, 7, 9, 8lmodvscl 15972 . . . 4
1715, 2, 4, 16syl3anc 1185 . . 3
185, 6, 7, 8, 9cphass 19178 . . 3
191, 13, 3, 17, 18syl13anc 1187 . 2
20 cphclm 19157 . . . . . 6 CMod
21203ad2ant1 979 . . . . 5 CMod
227, 8clmsscn 19109 . . . . 5 CMod
2321, 22syl 16 . . . 4
2423, 13sseldd 3351 . . 3
2523, 2sseldd 3351 . . . 4
2625cjcld 12006 . . 3
276, 5cphipcl 19159 . . . . 5
28273expb 1155 . . . 4