Theorem hdmap1val0

Description: Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 .) (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap1val0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap1val0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap1val0.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap1val0.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmap1val0.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap1val0.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmap1val0.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
	hdmap1val0.s	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
	hdmap1val0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap1val0.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	hdmap1val0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	hdmap1val0	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap1val0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap1val0.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap1val0.o	⊢ 0 = ( 0g ‘ 𝑈 )
5		hdmap1val0.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmap1val0.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
7		hdmap1val0.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
8		hdmap1val0.s	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
9		hdmap1val0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		hdmap1val0.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
11		hdmap1val0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12		eqid	⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
13		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
14		eqid	⊢ ( -g ‘ 𝐶 ) = ( -g ‘ 𝐶 )
15		eqid	⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
16		eqid	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
17	1 2 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	3 4	lmod0vcl	⊢ ( 𝑈 ∈ LMod → 0 ∈ 𝑉 )
19	17 18	syl	⊢ ( 𝜑 → 0 ∈ 𝑉 )
20	1 2 3 12 4 13 5 6 14 7 15 16 8 9 11 10 19	hdmap1val	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = if ( 0 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ℎ } ) ∧ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { ( 𝑋 ( -g ‘ 𝑈 ) 0 ) } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐹 ( -g ‘ 𝐶 ) ℎ ) } ) ) ) ) )
21		eqid	⊢ 0 = 0
22	21	iftruei	⊢ if ( 0 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ℎ } ) ∧ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { ( 𝑋 ( -g ‘ 𝑈 ) 0 ) } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐹 ( -g ‘ 𝐶 ) ℎ ) } ) ) ) ) = 𝑄
23	20 22	eqtrdi	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = 𝑄 )