# Metamath Proof Explorer

## Theorem ipassr2

Description: "Associative" law for inner product. Conjugate version of ipassr . (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 ipassr2

### 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 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}$
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 1 phlsrng ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$
12 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}$
13 7 4 srngcl
14 11 12 13 syl2an2r
15 1 2 3 4 5 6 7 ipassr
16 8 9 10 14 15 syl13anc
17 7 4 srngnvl
18 11 12 17 syl2an2r
19 18 oveq2d
20 16 19 eqtr2d