hlhilipval

Description: Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilip.h	$⊢ H = LHyp (K)$
	hlhilip.l	$⊢ L = DVecH (K) (W)$
	hlhilip.v	$⊢ V = {Base}_{L}$
	hlhilip.s	$⊢ S = HDMap (K) (W)$
	hlhilip.u	$⊢ U = HLHil (K) (W)$
	hlhilip.k	$⊢ φ \to (K \in HL \land W \in H)$
	hlhilip.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
	hlhilip.x	$⊢ φ \to X \in V$
	hlhilip.y	$⊢ φ \to Y \in V$
Assertion	hlhilipval	$⊢ φ \to X \underset{˙}{,} Y = S (Y) (X)$

Proof

Step	Hyp	Ref	Expression
1		hlhilip.h	$⊢ H = LHyp (K)$
2		hlhilip.l	$⊢ L = DVecH (K) (W)$
3		hlhilip.v	$⊢ V = {Base}_{L}$
4		hlhilip.s	$⊢ S = HDMap (K) (W)$
5		hlhilip.u	$⊢ U = HLHil (K) (W)$
6		hlhilip.k	$⊢ φ \to (K \in HL \land W \in H)$
7		hlhilip.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
8		hlhilip.x	$⊢ φ \to X \in V$
9		hlhilip.y	$⊢ φ \to Y \in V$
10		eqid	$⊢ (x \in V, y \in V ⟼ S (y) (x)) = (x \in V, y \in V ⟼ S (y) (x))$
11	1 2 3 4 5 6 10	hlhilip	$⊢ φ \to (x \in V, y \in V ⟼ S (y) (x)) = \cdot_{𝑖} (U)$
12	7 11	eqtr4id	$⊢ φ \to \underset{˙}{,} = (x \in V, y \in V ⟼ S (y) (x))$
13	12	oveqd	$⊢ φ \to X \underset{˙}{,} Y = X (x \in V, y \in V ⟼ S (y) (x)) Y$
14		fveq2	$⊢ x = X \to S (y) (x) = S (y) (X)$
15		fveq2	$⊢ y = Y \to S (y) = S (Y)$
16	15	fveq1d	$⊢ y = Y \to S (y) (X) = S (Y) (X)$
17		fvex	$⊢ S (Y) (X) \in V$
18	14 16 10 17	ovmpo	$⊢ (X \in V \land Y \in V) \to X (x \in V, y \in V ⟼ S (y) (x)) Y = S (Y) (X)$
19	8 9 18	syl2anc	$⊢ φ \to X (x \in V, y \in V ⟼ S (y) (x)) Y = S (Y) (X)$
20	13 19	eqtrd	$⊢ φ \to X \underset{˙}{,} Y = S (Y) (X)$

Metamath Proof Explorer

Theorem hlhilipval

Proof