Metamath Proof Explorer

Theorem lcdsca

Description: The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses lcdsca.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcdsca.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
lcdsca.o ⊢ 𝑂 = ( oppr ‘ 𝐹 )
lcdsca.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdsca.r ⊢ 𝑅 = ( Scalar ‘ 𝐶 )
lcdsca.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion lcdsca ( 𝜑 → 𝑅 = 𝑂 )

Proof

Step Hyp Ref Expression
1 lcdsca.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdsca.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
4 lcdsca.o ⊢ 𝑂 = ( oppr ‘ 𝐹 )
5 lcdsca.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcdsca.r ⊢ 𝑅 = ( Scalar ‘ 𝐶 )
7 lcdsca.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
10 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
11 eqid ⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
12 1 8 5 2 9 10 11 7 lcdval ⊢ ( 𝜑 → 𝐶 = ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
13 12 fveq2d ⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) = ( Scalar ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
14 fvex ⊢ ( LFnl ‘ 𝑈 ) ∈ V
15 14 rabex ⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V
16 eqid ⊢ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) = ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
17 eqid ⊢ ( Scalar ‘ ( LDual ‘ 𝑈 ) ) = ( Scalar ‘ ( LDual ‘ 𝑈 ) )
18 16 17 resssca ⊢ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V → ( Scalar ‘ ( LDual ‘ 𝑈 ) ) = ( Scalar ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
19 15 18 ax-mp ⊢ ( Scalar ‘ ( LDual ‘ 𝑈 ) ) = ( Scalar ‘ ( ( LDual ‘ 𝑈 ) ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
20 13 19 eqtr4di ⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) = ( Scalar ‘ ( LDual ‘ 𝑈 ) ) )
21 1 2 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
22 3 4 11 17 21 ldualsca ⊢ ( 𝜑 → ( Scalar ‘ ( LDual ‘ 𝑈 ) ) = 𝑂 )
23 20 22 eqtrd ⊢ ( 𝜑 → ( Scalar ‘ 𝐶 ) = 𝑂 )
24 6 23 syl5eq ⊢ ( 𝜑 → 𝑅 = 𝑂 )