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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipdir.f ⊢ 𝐾 = ( Base ‘ 𝐹 )
ipass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
ipass.p ⊢ × = ( .r ‘ 𝐹 )
ipassr.i ⊢ ∗ = ( *𝑟 ‘ 𝐹 )
Assertion ipassr2 ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ( 𝐴 , 𝐵 ) × 𝐶 ) = ( 𝐴 , ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ipdir.f ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 ipass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 ipass.p ⊢ × = ( .r ‘ 𝐹 )
7 ipassr.i ⊢ ∗ = ( *𝑟 ‘ 𝐹 )
8 simpl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝑊 ∈ PreHil )
9 simpr1 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐴 ∈ 𝑉 )
10 simpr2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐵 ∈ 𝑉 )
11 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
12 simpr3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐶 ∈ 𝐾 )
13 7 4 srngcl ⊢ ( ( 𝐹 ∈ *-Ring ∧ 𝐶 ∈ 𝐾 ) → ( ∗ ‘ 𝐶 ) ∈ 𝐾 )
14 11 12 13 syl2an2r ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ 𝐶 ) ∈ 𝐾 )
15 1 2 3 4 5 6 7 ipassr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ ( ∗ ‘ 𝐶 ) ∈ 𝐾 ) ) → ( 𝐴 , ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) = ( ( 𝐴 , 𝐵 ) × ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) ) )
16 8 9 10 14 15 syl13anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( 𝐴 , ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) = ( ( 𝐴 , 𝐵 ) × ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) ) )
17 7 4 srngnvl ⊢ ( ( 𝐹 ∈ *-Ring ∧ 𝐶 ∈ 𝐾 ) → ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) = 𝐶 )
18 11 12 17 syl2an2r ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) = 𝐶 )
19 18 oveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ( 𝐴 , 𝐵 ) × ( ∗ ‘ ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝐴 , 𝐵 ) × 𝐶 ) )
20 16 19 eqtr2d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ( 𝐴 , 𝐵 ) × 𝐶 ) = ( 𝐴 , ( ( ∗ ‘ 𝐶 ) · 𝐵 ) ) )