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 , 𝐴 ) = 𝑍 )