Theorem hdmapevec2

Description: The inner product of the reference vector E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of Holland95 p. 14 line 32, [ e , e ] =/= 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmapevec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapevec.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapevec.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapevec2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec2.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapevec2.i	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	hdmapevec2	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		hdmapevec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapevec.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapevec.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapevec.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapevec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		hdmapevec2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapevec2.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
8		hdmapevec2.i	⊢ 1 = ( 1r ‘ 𝑅 )
9	1 2 3 4 5	hdmapevec	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )
10		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
12		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
13		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
14		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
18	1 16 17 6 11 14 2 5	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) )
19	1 6 10 11 12 13 14 7 15 3 5 18	hvmapval	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) = ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) ) )
20	9 19	eqtrd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) ) )
21	20	fveq1d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = ( ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) ) ‘ 𝐸 ) )
22		eqid	⊢ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) ) = ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) )
23	1 10 6 11 12 13 14 7 15 8 5 18 22	dochfl1	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( Base ‘ 𝑈 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ 𝑅 ) ∃ 𝑤 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝐸 } ) 𝑣 = ( 𝑤 ( +g ‘ 𝑈 ) ( 𝑘 ( ·𝑠 ‘ 𝑈 ) 𝐸 ) ) ) ) ‘ 𝐸 ) = 1 )
24	21 23	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = 1 )