Metamath Proof Explorer


Theorem ip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (Contributed by NM, 5-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h , = ( ·𝑖𝑊 )
phllmhm.v 𝑉 = ( Base ‘ 𝑊 )
ip0l.z 𝑍 = ( 0g𝐹 )
ip0l.o 0 = ( 0g𝑊 )
Assertion ip0l ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → ( 0 , 𝐴 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 phlsrng.f 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h , = ( ·𝑖𝑊 )
3 phllmhm.v 𝑉 = ( Base ‘ 𝑊 )
4 ip0l.z 𝑍 = ( 0g𝐹 )
5 ip0l.o 0 = ( 0g𝑊 )
6 phllmod ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
7 lmodgrp ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
8 3 5 grpidcl ( 𝑊 ∈ Grp → 0𝑉 )
9 6 7 8 3syl ( 𝑊 ∈ PreHil → 0𝑉 )
10 9 adantr ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → 0𝑉 )
11 oveq1 ( 𝑥 = 0 → ( 𝑥 , 𝐴 ) = ( 0 , 𝐴 ) )
12 eqid ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) = ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) )
13 ovex ( 0 , 𝐴 ) ∈ V
14 11 12 13 fvmpt ( 0𝑉 → ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = ( 0 , 𝐴 ) )
15 10 14 syl ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = ( 0 , 𝐴 ) )
16 1 2 3 12 phllmhm ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
17 lmghm ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) → ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) )
18 rlm0 ( 0g𝐹 ) = ( 0g ‘ ( ringLMod ‘ 𝐹 ) )
19 4 18 eqtri 𝑍 = ( 0g ‘ ( ringLMod ‘ 𝐹 ) )
20 5 19 ghmid ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) → ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = 𝑍 )
21 16 17 20 3syl ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → ( ( 𝑥𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = 𝑍 )
22 15 21 eqtr3d ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉 ) → ( 0 , 𝐴 ) = 𝑍 )