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 = Scalar W
phllmhm.h , ˙ = 𝑖 W
phllmhm.v V = Base W
ipdir.f K = Base F
ipass.s · ˙ = W
ipass.p × ˙ = F
ipassr.i ˙ = * F
Assertion ipassr2 W PreHil A V B V C K A , ˙ B × ˙ C = A , ˙ ˙ C · ˙ B

Proof

Step Hyp Ref Expression
1 phlsrng.f F = Scalar W
2 phllmhm.h , ˙ = 𝑖 W
3 phllmhm.v V = Base W
4 ipdir.f K = Base F
5 ipass.s · ˙ = W
6 ipass.p × ˙ = F
7 ipassr.i ˙ = * F
8 simpl W PreHil A V B V C K W PreHil
9 simpr1 W PreHil A V B V C K A V
10 simpr2 W PreHil A V B V C K B V
11 1 phlsrng W PreHil F *-Ring
12 simpr3 W PreHil A V B V C K C K
13 7 4 srngcl F *-Ring C K ˙ C K
14 11 12 13 syl2an2r W PreHil A V B V C K ˙ C K
15 1 2 3 4 5 6 7 ipassr W PreHil A V B V ˙ C K A , ˙ ˙ C · ˙ B = A , ˙ B × ˙ ˙ ˙ C
16 8 9 10 14 15 syl13anc W PreHil A V B V C K A , ˙ ˙ C · ˙ B = A , ˙ B × ˙ ˙ ˙ C
17 7 4 srngnvl F *-Ring C K ˙ ˙ C = C
18 11 12 17 syl2an2r W PreHil A V B V C K ˙ ˙ C = C
19 18 oveq2d W PreHil A V B V C K A , ˙ B × ˙ ˙ ˙ C = A , ˙ B × ˙ C
20 16 19 eqtr2d W PreHil A V B V C K A , ˙ B × ˙ C = A , ˙ ˙ C · ˙ B