Metamath Proof Explorer

Theorem lcd0v

Description: The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcd0v.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcd0v.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcd0v.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lcd0v.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
lcd0v.z ⊢ 0 = ( 0g ‘ 𝑅 )
lcd0v.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcd0v.o ⊢ 𝑂 = ( 0g ‘ 𝐶 )
lcd0v.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion lcd0v ( 𝜑 → 𝑂 = ( 𝑉 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 lcd0v.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcd0v.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcd0v.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 lcd0v.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5 lcd0v.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 lcd0v.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 lcd0v.o ⊢ 𝑂 = ( 0g ‘ 𝐶 )
8 lcd0v.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
10 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
11 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
12 eqid ⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
13 1 9 6 2 10 11 12 8 lcdval ⊢ ( 𝜑 → 𝐶 = ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
14 13 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝐶 ) = ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
15 7 14 syl5eq ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
16 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
17 12 16 lduallmod ⊢ ( 𝜑 → ( LDual ‘ 𝑈 ) ∈ LMod )
18 eqid ⊢ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) = ( LSubSp ‘ ( LDual ‘ 𝑈 ) )
19 eqid ⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) }
20 1 2 9 10 11 12 18 19 8 lclkr ⊢ ( 𝜑 → { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) )
21 eqid ⊢ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) = ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
22 eqid ⊢ ( 0g ‘ ( LDual ‘ 𝑈 ) ) = ( 0g ‘ ( LDual ‘ 𝑈 ) )
23 eqid ⊢ ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) = ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
24 21 22 23 18 lss0v ⊢ ( ( ( LDual ‘ 𝑈 ) ∈ LMod ∧ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ) → ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) = ( 0g ‘ ( LDual ‘ 𝑈 ) ) )
25 17 20 24 syl2anc ⊢ ( 𝜑 → ( 0g ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) = ( 0g ‘ ( LDual ‘ 𝑈 ) ) )
26 3 4 5 12 22 16 ldual0v ⊢ ( 𝜑 → ( 0g ‘ ( LDual ‘ 𝑈 ) ) = ( 𝑉 × { 0 } ) )
27 15 25 26 3eqtrd ⊢ ( 𝜑 → 𝑂 = ( 𝑉 × { 0 } ) )