Metamath Proof Explorer

Theorem cphassr

Description: "Associative" law for second argument of inner product (compare cphass ). See ipassr , his52 . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
cphipcj.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
cphass.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
cphass.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
cphass.s ⊒ Β· = ( ·𝑠 β€˜ π‘Š )
Assertion cphassr ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( 𝐡 , ( 𝐴 Β· 𝐢 ) ) = ( ( βˆ— β€˜ 𝐴 ) Β· ( 𝐡 , 𝐢 ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
2 cphipcj.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
3 cphass.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
4 cphass.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
5 cphass.s ⊒ Β· = ( ·𝑠 β€˜ π‘Š )
6 cphclm ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ β„‚Mod )
7 6 adantr ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ π‘Š ∈ β„‚Mod )
8 3 clmmul ⊒ ( π‘Š ∈ β„‚Mod β†’ Β· = ( .r β€˜ 𝐹 ) )
9 7 8 syl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ Β· = ( .r β€˜ 𝐹 ) )
10 eqidd ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( 𝐡 , 𝐢 ) = ( 𝐡 , 𝐢 ) )
11 3 clmcj ⊒ ( π‘Š ∈ β„‚Mod β†’ βˆ— = ( *π‘Ÿ β€˜ 𝐹 ) )
12 7 11 syl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ βˆ— = ( *π‘Ÿ β€˜ 𝐹 ) )
13 12 fveq1d ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( βˆ— β€˜ 𝐴 ) = ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝐴 ) )
14 9 10 13 oveq123d ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( ( 𝐡 , 𝐢 ) Β· ( βˆ— β€˜ 𝐴 ) ) = ( ( 𝐡 , 𝐢 ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝐴 ) ) )
15 3 4 clmsscn ⊒ ( π‘Š ∈ β„‚Mod β†’ 𝐾 βŠ† β„‚ )
16 7 15 syl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ 𝐾 βŠ† β„‚ )
17 simpr1 ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ 𝐴 ∈ 𝐾 )
18 16 17 sseldd ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ 𝐴 ∈ β„‚ )
19 18 cjcld ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( βˆ— β€˜ 𝐴 ) ∈ β„‚ )
20 2 1 cphipcl ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) β†’ ( 𝐡 , 𝐢 ) ∈ β„‚ )
21 20 3adant3r1 ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( 𝐡 , 𝐢 ) ∈ β„‚ )
22 19 21 mulcomd ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( ( βˆ— β€˜ 𝐴 ) Β· ( 𝐡 , 𝐢 ) ) = ( ( 𝐡 , 𝐢 ) Β· ( βˆ— β€˜ 𝐴 ) ) )
23 cphphl ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )
24 3anrot ⊒ ( ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ↔ ( 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) )
25 24 biimpi ⊒ ( ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) β†’ ( 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) )
26 eqid ⊒ ( .r β€˜ 𝐹 ) = ( .r β€˜ 𝐹 )
27 eqid ⊒ ( *π‘Ÿ β€˜ 𝐹 ) = ( *π‘Ÿ β€˜ 𝐹 )
28 3 1 2 4 5 26 27 ipassr ⊒ ( ( π‘Š ∈ PreHil ∧ ( 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) ) β†’ ( 𝐡 , ( 𝐴 Β· 𝐢 ) ) = ( ( 𝐡 , 𝐢 ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝐴 ) ) )
29 23 25 28 syl2an ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( 𝐡 , ( 𝐴 Β· 𝐢 ) ) = ( ( 𝐡 , 𝐢 ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝐴 ) ) )
30 14 22 29 3eqtr4rd ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐡 ∈ 𝑉 ∧ 𝐢 ∈ 𝑉 ) ) β†’ ( 𝐡 , ( 𝐴 Β· 𝐢 ) ) = ( ( βˆ— β€˜ 𝐴 ) Β· ( 𝐡 , 𝐢 ) ) )