lcdvbase

Description: Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvbase.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbase.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbase.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdvbase.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbase.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcdvbase.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcdvbase.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcdvbase.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdvbase	⊢ ( 𝜑 → 𝑉 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lcdvbase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvbase.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvbase.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
4		lcdvbase.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
5		lcdvbase.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		lcdvbase.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcdvbase.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		lcdvbase.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
9		lcdvbase.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
11	1 2 3 5 6 7 10 9 8	lcdval2	⊢ ( 𝜑 → 𝐶 = ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) )
12	11	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) ) )
13	4 12	syl5eq	⊢ ( 𝜑 → 𝑉 = ( Base ‘ ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) ) )
14		ssrab2	⊢ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ⊆ 𝐹
15	8 14	eqsstri	⊢ 𝐵 ⊆ 𝐹
16		eqid	⊢ ( Base ‘ ( LDual ‘ 𝑈 ) ) = ( Base ‘ ( LDual ‘ 𝑈 ) )
17	1 5 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	6 10 16 17	ldualvbase	⊢ ( 𝜑 → ( Base ‘ ( LDual ‘ 𝑈 ) ) = 𝐹 )
19	15 18	sseqtrrid	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( LDual ‘ 𝑈 ) ) )
20		eqid	⊢ ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) = ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 )
21	20 16	ressbas2	⊢ ( 𝐵 ⊆ ( Base ‘ ( LDual ‘ 𝑈 ) ) → 𝐵 = ( Base ‘ ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) ) )
22	19 21	syl	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( LDual ‘ 𝑈 ) ↾_s 𝐵 ) ) )
23	13 22	eqtr4d	⊢ ( 𝜑 → 𝑉 = 𝐵 )

Metamath Proof Explorer

Theorem lcdvbase

Proof