Metamath Proof Explorer


Theorem lcfrvalsnN

Description: Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcfrvalsn.h H = LHyp K
lcfrvalsn.o ˙ = ocH K W
lcfrvalsn.u U = DVecH K W
lcfrvalsn.f F = LFnl U
lcfrvalsn.l L = LKer U
lcfrvalsn.d D = LDual U
lcfrvalsn.n N = LSpan D
lcfrvalsn.k φ K HL W H
lcfrvalsn.g φ G F
lcfrvalsn.q Q = f R ˙ L f
lcfrvalsn.r R = N G
Assertion lcfrvalsnN φ Q = ˙ L G

Proof

Step Hyp Ref Expression
1 lcfrvalsn.h H = LHyp K
2 lcfrvalsn.o ˙ = ocH K W
3 lcfrvalsn.u U = DVecH K W
4 lcfrvalsn.f F = LFnl U
5 lcfrvalsn.l L = LKer U
6 lcfrvalsn.d D = LDual U
7 lcfrvalsn.n N = LSpan D
8 lcfrvalsn.k φ K HL W H
9 lcfrvalsn.g φ G F
10 lcfrvalsn.q Q = f R ˙ L f
11 lcfrvalsn.r R = N G
12 eliun x f R ˙ L f f R x ˙ L f
13 11 eleq2i f R f N G
14 8 adantr φ f N G K HL W H
15 eqid Base U = Base U
16 1 3 8 dvhlmod φ U LMod
17 16 adantr φ f N G U LMod
18 6 16 lduallmod φ D LMod
19 eqid Base D = Base D
20 4 6 19 16 9 ldualelvbase φ G Base D
21 eqid LSubSp D = LSubSp D
22 19 21 7 lspsncl D LMod G Base D N G LSubSp D
23 18 20 22 syl2anc φ N G LSubSp D
24 19 21 lssel N G LSubSp D f N G f Base D
25 23 24 sylan φ f N G f Base D
26 4 6 19 16 ldualvbase φ Base D = F
27 26 adantr φ f N G Base D = F
28 25 27 eleqtrd φ f N G f F
29 15 4 5 17 28 lkrssv φ f N G L f Base U
30 eqid Scalar D = Scalar D
31 eqid Base Scalar D = Base Scalar D
32 eqid D = D
33 30 31 19 32 7 lspsnel D LMod G Base D f N G k Base Scalar D f = k D G
34 18 20 33 syl2anc φ f N G k Base Scalar D f = k D G
35 eqid Scalar U = Scalar U
36 eqid Base Scalar U = Base Scalar U
37 35 36 6 30 31 16 ldualsbase φ Base Scalar D = Base Scalar U
38 37 rexeqdv φ k Base Scalar D f = k D G k Base Scalar U f = k D G
39 34 38 bitrd φ f N G k Base Scalar U f = k D G
40 39 biimpa φ f N G k Base Scalar U f = k D G
41 1 3 8 dvhlvec φ U LVec
42 41 adantr φ f N G U LVec
43 9 adantr φ f N G G F
44 35 36 4 5 6 32 42 43 28 lkrss2N φ f N G L G L f k Base Scalar U f = k D G
45 40 44 mpbird φ f N G L G L f
46 1 3 15 2 dochss K HL W H L f Base U L G L f ˙ L f ˙ L G
47 14 29 45 46 syl3anc φ f N G ˙ L f ˙ L G
48 47 sseld φ f N G x ˙ L f x ˙ L G
49 48 ex φ f N G x ˙ L f x ˙ L G
50 13 49 syl5bi φ f R x ˙ L f x ˙ L G
51 50 rexlimdv φ f R x ˙ L f x ˙ L G
52 19 7 lspsnid D LMod G Base D G N G
53 18 20 52 syl2anc φ G N G
54 53 11 eleqtrrdi φ G R
55 2fveq3 f = G ˙ L f = ˙ L G
56 55 eleq2d f = G x ˙ L f x ˙ L G
57 56 rspcev G R x ˙ L G f R x ˙ L f
58 54 57 sylan φ x ˙ L G f R x ˙ L f
59 58 ex φ x ˙ L G f R x ˙ L f
60 51 59 impbid φ f R x ˙ L f x ˙ L G
61 12 60 syl5bb φ x f R ˙ L f x ˙ L G
62 61 eqrdv φ f R ˙ L f = ˙ L G
63 10 62 syl5eq φ Q = ˙ L G