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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipdir.f ⊢ 𝐾 = ( Base ‘ 𝐹 )
ipass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
ipass.p ⊢ × = ( .r ‘ 𝐹 )
ipassr.i ⊢ ∗ = ( *𝑟 ‘ 𝐹 )
Assertion ipassr ( ( 𝑊 ∈ 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 simpr3 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐶 ∈ 𝐾 )
10 simpr2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐵 ∈ 𝑉 )
11 simpr1 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐴 ∈ 𝑉 )
12 1 2 3 4 5 6 ipass ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐶 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( ( 𝐶 · 𝐵 ) , 𝐴 ) = ( 𝐶 × ( 𝐵 , 𝐴 ) ) )
13 8 9 10 11 12 syl13anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ( 𝐶 · 𝐵 ) , 𝐴 ) = ( 𝐶 × ( 𝐵 , 𝐴 ) ) )
14 13 fveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ ( ( 𝐶 · 𝐵 ) , 𝐴 ) ) = ( ∗ ‘ ( 𝐶 × ( 𝐵 , 𝐴 ) ) ) )
15 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
16 15 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝑊 ∈ LMod )
17 3 1 5 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐶 · 𝐵 ) ∈ 𝑉 )
18 16 9 10 17 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( 𝐶 · 𝐵 ) ∈ 𝑉 )
19 1 2 3 7 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐶 · 𝐵 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ∗ ‘ ( ( 𝐶 · 𝐵 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐶 · 𝐵 ) ) )
20 8 18 11 19 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ ( ( 𝐶 · 𝐵 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐶 · 𝐵 ) ) )
21 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
22 21 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → 𝐹 ∈ *-Ring )
23 1 2 3 4 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 , 𝐴 ) ∈ 𝐾 )
24 8 10 11 23 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( 𝐵 , 𝐴 ) ∈ 𝐾 )
25 7 4 6 srngmul ⊢ ( ( 𝐹 ∈ *-Ring ∧ 𝐶 ∈ 𝐾 ∧ ( 𝐵 , 𝐴 ) ∈ 𝐾 ) → ( ∗ ‘ ( 𝐶 × ( 𝐵 , 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 , 𝐴 ) ) × ( ∗ ‘ 𝐶 ) ) )
26 22 9 24 25 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ ( 𝐶 × ( 𝐵 , 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 , 𝐴 ) ) × ( ∗ ‘ 𝐶 ) ) )
27 14 20 26 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( 𝐴 , ( 𝐶 · 𝐵 ) ) = ( ( ∗ ‘ ( 𝐵 , 𝐴 ) ) × ( ∗ ‘ 𝐶 ) ) )
28 1 2 3 7 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) )
29 8 10 11 28 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ∗ ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) )
30 29 oveq1d ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( ( ∗ ‘ ( 𝐵 , 𝐴 ) ) × ( ∗ ‘ 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) × ( ∗ ‘ 𝐶 ) ) )
31 27 30 eqtrd ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾 ) ) → ( 𝐴 , ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 , 𝐵 ) × ( ∗ ‘ 𝐶 ) ) )