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