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	$⊢ F = Scalar (W)$
	phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	phllmhm.v	$⊢ V = {Base}_{W}$
	ip0l.z	$⊢ Z = 0_{F}$
	ip0l.o	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	ip0r	$⊢ (W \in PreHil \land A \in V) \to A \underset{˙}{,} \underset{˙}{0} = Z$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$⊢ F = Scalar (W)$
2		phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		phllmhm.v	$⊢ V = {Base}_{W}$
4		ip0l.z	$⊢ Z = 0_{F}$
5		ip0l.o	$⊢ \underset{˙}{0} = 0_{W}$
6	1 2 3 4 5	ip0l	$⊢ (W \in PreHil \land A \in V) \to \underset{˙}{0} \underset{˙}{,} A = Z$
7	6	fveq2d	$⊢ (W \in PreHil \land A \in V) \to {(\underset{˙}{0} \underset{˙}{,} A)}^{_{F}} = Z^{_{F}}$
8		phllmod	$⊢ W \in PreHil \to W \in LMod$
9	8	adantr	$⊢ (W \in PreHil \land A \in V) \to W \in LMod$
10	3 5	lmod0vcl	$⊢ W \in LMod \to \underset{˙}{0} \in V$
11	9 10	syl	$⊢ (W \in PreHil \land A \in V) \to \underset{˙}{0} \in V$
12		eqid	$⊢ _{F} = _{F}$
13	1 2 3 12	ipcj	$⊢ (W \in PreHil \land \underset{˙}{0} \in V \land A \in V) \to {(\underset{˙}{0} \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} \underset{˙}{0}$
14	13	3expa	$⊢ ((W \in PreHil \land \underset{˙}{0} \in V) \land A \in V) \to {(\underset{˙}{0} \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} \underset{˙}{0}$
15	14	an32s	$⊢ ((W \in PreHil \land A \in V) \land \underset{˙}{0} \in V) \to {(\underset{˙}{0} \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} \underset{˙}{0}$
16	11 15	mpdan	$⊢ (W \in PreHil \land A \in V) \to {(\underset{˙}{0} \underset{˙}{,} A)}^{*_{F}} = A \underset{˙}{,} \underset{˙}{0}$
17	1	phlsrng	$⊢ W \in PreHil \to F \in *-Ring$
18	17	adantr	$⊢ (W \in PreHil \land A \in V) \to F \in *-Ring$
19	12 4	srng0	$⊢ F \in -Ring \to Z^{_{F}} = Z$
20	18 19	syl	$⊢ (W \in PreHil \land A \in V) \to Z^{*_{F}} = Z$
21	7 16 20	3eqtr3d	$⊢ (W \in PreHil \land A \in V) \to A \underset{˙}{,} \underset{˙}{0} = Z$

Metamath Proof Explorer

Theorem ip0r

Proof