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 = opp r ⁡ 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 = opp r ⁡ 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 syl5eq ⊢ φ → R = O