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