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 ⊢H=LHyp⁡K
lcdsca.u ⊢U=DVecH⁡K⁡W
lcdsca.f ⊢F=Scalar⁡U
lcdsca.o ⊢O=oppr⁡F
lcdsca.c ⊢C=LCDual⁡K⁡W
lcdsca.r ⊢R=Scalar⁡C
lcdsca.k ⊢φ→K∈HL∧W∈H
Assertion lcdsca ⊢φ→R=O

Proof

Step Hyp Ref Expression
1 lcdsca.h ⊢H=LHyp⁡K
2 lcdsca.u ⊢U=DVecH⁡K⁡W
3 lcdsca.f ⊢F=Scalar⁡U
4 lcdsca.o ⊢O=oppr⁡F
5 lcdsca.c ⊢C=LCDual⁡K⁡W
6 lcdsca.r ⊢R=Scalar⁡C
7 lcdsca.k ⊢φ→K∈HL∧W∈H
8 eqid ⊢ocH⁡K⁡W=ocH⁡K⁡W
9 eqid ⊢LFnl⁡U=LFnl⁡U
10 eqid ⊢LKer⁡U=LKer⁡U
11 eqid ⊢LDual⁡U=LDual⁡U
12 1 8 5 2 9 10 11 7 lcdval ⊢φ→C=LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
13 12 fveq2d ⊢φ→Scalar⁡C=Scalar⁡LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
14 fvex ⊢LFnl⁡U∈V
15 14 rabex ⊢f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f∈V
16 eqid ⊢LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f=LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
17 eqid ⊢Scalar⁡LDual⁡U=Scalar⁡LDual⁡U
18 16 17 resssca ⊢f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f∈V→Scalar⁡LDual⁡U=Scalar⁡LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
19 15 18 ax-mp ⊢Scalar⁡LDual⁡U=Scalar⁡LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
20 13 19 eqtr4di ⊢φ→Scalar⁡C=Scalar⁡LDual⁡U
21 1 2 7 dvhlmod ⊢φ→U∈LMod
22 3 4 11 17 21 ldualsca ⊢φ→Scalar⁡LDual⁡U=O
23 20 22 eqtrd ⊢φ→Scalar⁡C=O
24 6 23 eqtrid ⊢φ→R=O