# Metamath Proof Explorer

## Theorem ipassr

Description: "Associative" law for second argument of inner product (compare ipass ). (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
phllmhm.h
phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ipdir.f ${⊢}{K}={\mathrm{Base}}_{{F}}$
ipass.s
ipass.p
ipassr.i
Assertion ipassr

### Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 phllmhm.h
3 phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 ipdir.f ${⊢}{K}={\mathrm{Base}}_{{F}}$
5 ipass.s
6 ipass.p
7 ipassr.i
8 simpl ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {W}\in \mathrm{PreHil}$
9 simpr3 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {C}\in {K}$
10 simpr2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {B}\in {V}$
11 simpr1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {A}\in {V}$
12 1 2 3 4 5 6 ipass
13 8 9 10 11 12 syl13anc
14 13 fveq2d
15 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
16 15 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {W}\in \mathrm{LMod}$
17 3 1 5 4 lmodvscl
18 16 9 10 17 syl3anc
19 1 2 3 7 ipcj
20 8 18 11 19 syl3anc
21 1 phlsrng ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$
22 21 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {K}\right)\right)\to {F}\in \mathrm{*-Ring}$
23 1 2 3 4 ipcl
24 8 10 11 23 syl3anc
25 7 4 6 srngmul
26 22 9 24 25 syl3anc
27 14 20 26 3eqtr3d
28 1 2 3 7 ipcj
29 8 10 11 28 syl3anc
30 29 oveq1d
31 27 30 eqtrd