Theorem lcdvs

Description: Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvs.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcdvs.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lcdvs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvs.m	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	lcdvs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdvs	⊢ ( 𝜑 → ∙ = · )

Proof

Step	Hyp	Ref	Expression
1		lcdvs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvs.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
4		lcdvs.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
5		lcdvs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		lcdvs.m	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
7		lcdvs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
10		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
11	1 8 5 2 9 10 3 7	lcdval	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
12	11	fveq2d	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
13		fvex	⊢ ( LFnl ‘ 𝑈 ) ∈ V
14	13	rabex	⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V
15		eqid	⊢ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
16	15 4	ressvsca	⊢ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V → · = ( ·𝑠 ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
17	14 16	ax-mp	⊢ · = ( ·𝑠 ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
18	12 6 17	3eqtr4g	⊢ ( 𝜑 → ∙ = · )