Metamath Proof Explorer

Theorem ip0r

Description: Inner product with a zero second argument. (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 ip0r ( ( 𝑊 ∈ 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 1 2 3 4 5 ip0l ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 0 , 𝐴 ) = 𝑍 )
7 6 fveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 0 , 𝐴 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) )
8 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
9 8 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ LMod )
10 3 5 lmod0vcl ⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝑉 )
11 9 10 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 0 ∈ 𝑉 )
12 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
13 1 2 3 12 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ 0 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 0 , 𝐴 ) ) = ( 𝐴 , 0 ) )
14 13 3expa ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 0 ∈ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 0 , 𝐴 ) ) = ( 𝐴 , 0 ) )
15 14 an32s ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) ∧ 0 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 0 , 𝐴 ) ) = ( 𝐴 , 0 ) )
16 11 15 mpdan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 0 , 𝐴 ) ) = ( 𝐴 , 0 ) )
17 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
18 17 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ *-Ring )
19 12 4 srng0 ⊢ ( 𝐹 ∈ *-Ring → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) = 𝑍 )
20 18 19 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) = 𝑍 )
21 7 16 20 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 0 ) = 𝑍 )