Metamath Proof Explorer

Theorem lcdlsp

Description: Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdlsp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcdlsp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdlsp.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lcdlsp.m ⊢ 𝑀 = ( LSpan ‘ 𝐷 )
lcdlsp.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdlsp.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
lcdlsp.n ⊢ 𝑁 = ( LSpan ‘ 𝐶 )
lcdlsp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcdlsp.g ⊢ ( 𝜑 → 𝐺 ⊆ 𝐹 )
Assertion lcdlsp ( 𝜑 → ( 𝑁 ‘ 𝐺 ) = ( 𝑀 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lcdlsp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdlsp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdlsp.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
4 lcdlsp.m ⊢ 𝑀 = ( LSpan ‘ 𝐷 )
5 lcdlsp.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcdlsp.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
7 lcdlsp.n ⊢ 𝑁 = ( LSpan ‘ 𝐶 )
8 lcdlsp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 lcdlsp.g ⊢ ( 𝜑 → 𝐺 ⊆ 𝐹 )
10 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
12 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
13 1 10 5 2 11 12 3 8 lcdval ⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
14 13 fveq2d ⊢ ( 𝜑 → ( LSpan ‘ 𝐶 ) = ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
15 7 14 syl5eq ⊢ ( 𝜑 → 𝑁 = ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
16 15 fveq1d ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐺 ) = ( ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) ‘ 𝐺 ) )
17 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
18 3 17 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
19 eqid ⊢ ( LSubSp ‘ 𝐷 ) = ( LSubSp ‘ 𝐷 )
20 eqid ⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) }
21 1 2 10 11 12 3 19 20 8 lclkr ⊢ ( 𝜑 → { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ 𝐷 ) )
22 1 10 5 6 2 11 12 20 8 lcdvbase ⊢ ( 𝜑 → 𝐹 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
23 9 22 sseqtrd ⊢ ( 𝜑 → 𝐺 ⊆ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
24 eqid ⊢ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
25 eqid ⊢ ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) = ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
26 24 4 25 19 lsslsp ⊢ ( ( 𝐷 ∈ LMod ∧ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ 𝐷 ) ∧ 𝐺 ⊆ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) → ( 𝑀 ‘ 𝐺 ) = ( ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) ‘ 𝐺 ) )
27 18 21 23 26 syl3anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐺 ) = ( ( LSpan ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) ‘ 𝐺 ) )
28 16 27 eqtr4d ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐺 ) = ( 𝑀 ‘ 𝐺 ) )