Metamath Proof Explorer

Theorem lcfr

Description: Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015)

Ref Expression
Hypotheses lcfr.h ⊢ H = LHyp ⁡ K
lcfr.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
lcfr.u ⊢ U = DVecH ⁡ K ⁡ W
lcfr.s ⊢ S = LSubSp ⁡ U
lcfr.f ⊢ F = LFnl ⁡ U
lcfr.l ⊢ L = LKer ⁡ U
lcfr.d ⊢ D = LDual ⁡ U
lcfr.t ⊢ T = LSubSp ⁡ D
lcfr.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
lcfr.q ⊢ Q = ⋃ g ∈ R ⊥ ˙ ⁡ L ⁡ g
lcfr.k ⊢ φ → K ∈ HL ∧ W ∈ H
lcfr.r ⊢ φ → R ∈ T
lcfr.rs ⊢ φ → R ⊆ C
Assertion lcfr ⊢ φ → Q ∈ S

Proof

Step Hyp Ref Expression
1 lcfr.h ⊢ H = LHyp ⁡ K
2 lcfr.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 lcfr.u ⊢ U = DVecH ⁡ K ⁡ W
4 lcfr.s ⊢ S = LSubSp ⁡ U
5 lcfr.f ⊢ F = LFnl ⁡ U
6 lcfr.l ⊢ L = LKer ⁡ U
7 lcfr.d ⊢ D = LDual ⁡ U
8 lcfr.t ⊢ T = LSubSp ⁡ D
9 lcfr.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
10 lcfr.q ⊢ Q = ⋃ g ∈ R ⊥ ˙ ⁡ L ⁡ g
11 lcfr.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 lcfr.r ⊢ φ → R ∈ T
13 lcfr.rs ⊢ φ → R ⊆ C
14 2fveq3 ⊢ g = h → ⊥ ˙ ⁡ L ⁡ g = ⊥ ˙ ⁡ L ⁡ h
15 14 cbviunv ⊢ ⋃ g ∈ R ⊥ ˙ ⁡ L ⁡ g = ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h
16 10 15 eqtri ⊢ Q = ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h
17 11 adantr ⊢ φ ∧ h ∈ R → K ∈ HL ∧ W ∈ H
18 eqid ⊢ Base U = Base U
19 1 3 11 dvhlmod ⊢ φ → U ∈ LMod
20 19 adantr ⊢ φ ∧ h ∈ R → U ∈ LMod
21 eqid ⊢ Base D = Base D
22 21 8 lssss ⊢ R ∈ T → R ⊆ Base D
23 12 22 syl ⊢ φ → R ⊆ Base D
24 5 7 21 19 ldualvbase ⊢ φ → Base D = F
25 23 24 sseqtrd ⊢ φ → R ⊆ F
26 25 sselda ⊢ φ ∧ h ∈ R → h ∈ F
27 18 5 6 20 26 lkrssv ⊢ φ ∧ h ∈ R → L ⁡ h ⊆ Base U
28 1 3 18 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ h ⊆ Base U → ⊥ ˙ ⁡ L ⁡ h ⊆ Base U
29 17 27 28 syl2anc ⊢ φ ∧ h ∈ R → ⊥ ˙ ⁡ L ⁡ h ⊆ Base U
30 29 ralrimiva ⊢ φ → ∀ h ∈ R ⊥ ˙ ⁡ L ⁡ h ⊆ Base U
31 iunss ⊢ ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h ⊆ Base U ↔ ∀ h ∈ R ⊥ ˙ ⁡ L ⁡ h ⊆ Base U
32 30 31 sylibr ⊢ φ → ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h ⊆ Base U
33 16 32 eqsstrid ⊢ φ → Q ⊆ Base U
34 16 a1i ⊢ φ → Q = ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h
35 7 19 lduallmod ⊢ φ → D ∈ LMod
36 eqid ⊢ 0 D = 0 D
37 36 8 lss0cl ⊢ D ∈ LMod ∧ R ∈ T → 0 D ∈ R
38 35 12 37 syl2anc ⊢ φ → 0 D ∈ R
39 5 7 36 19 ldual0vcl ⊢ φ → 0 D ∈ F
40 18 5 6 19 39 lkrssv ⊢ φ → L ⁡ 0 D ⊆ Base U
41 1 3 18 4 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ 0 D ⊆ Base U → ⊥ ˙ ⁡ L ⁡ 0 D ∈ S
42 11 40 41 syl2anc ⊢ φ → ⊥ ˙ ⁡ L ⁡ 0 D ∈ S
43 eqid ⊢ 0 U = 0 U
44 43 4 lss0cl ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ L ⁡ 0 D ∈ S → 0 U ∈ ⊥ ˙ ⁡ L ⁡ 0 D
45 19 42 44 syl2anc ⊢ φ → 0 U ∈ ⊥ ˙ ⁡ L ⁡ 0 D
46 2fveq3 ⊢ h = 0 D → ⊥ ˙ ⁡ L ⁡ h = ⊥ ˙ ⁡ L ⁡ 0 D
47 46 eleq2d ⊢ h = 0 D → 0 U ∈ ⊥ ˙ ⁡ L ⁡ h ↔ 0 U ∈ ⊥ ˙ ⁡ L ⁡ 0 D
48 47 rspcev ⊢ 0 D ∈ R ∧ 0 U ∈ ⊥ ˙ ⁡ L ⁡ 0 D → ∃ h ∈ R 0 U ∈ ⊥ ˙ ⁡ L ⁡ h
49 38 45 48 syl2anc ⊢ φ → ∃ h ∈ R 0 U ∈ ⊥ ˙ ⁡ L ⁡ h
50 eliun ⊢ 0 U ∈ ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h ↔ ∃ h ∈ R 0 U ∈ ⊥ ˙ ⁡ L ⁡ h
51 49 50 sylibr ⊢ φ → 0 U ∈ ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h
52 51 ne0d ⊢ φ → ⋃ h ∈ R ⊥ ˙ ⁡ L ⁡ h ≠ ∅
53 34 52 eqnetrd ⊢ φ → Q ≠ ∅
54 eqid ⊢ + U = + U
55 rabeq ⊢ F = LFnl ⁡ U → f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f = f ∈ LFnl ⁡ U | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
56 5 55 ax-mp ⊢ f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f = f ∈ LFnl ⁡ U | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
57 9 56 eqtri ⊢ C = f ∈ LFnl ⁡ U | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
58 11 adantr ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → K ∈ HL ∧ W ∈ H
59 12 adantr ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → R ∈ T
60 13 adantr ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → R ⊆ C
61 simpr2 ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → a ∈ Q
62 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
63 eqid ⊢ Base Scalar ⁡ U = Base Scalar ⁡ U
64 eqid ⊢ ⋅ U = ⋅ U
65 simpr1 ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → x ∈ Base Scalar ⁡ U
66 1 2 3 18 5 6 7 8 58 59 16 61 62 63 64 65 lcfrlem5 ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → x ⋅ U a ∈ Q
67 simpr3 ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → b ∈ Q
68 1 2 3 54 5 6 7 8 57 16 58 59 60 66 67 lcfrlem42 ⊢ φ ∧ x ∈ Base Scalar ⁡ U ∧ a ∈ Q ∧ b ∈ Q → x ⋅ U a + U b ∈ Q
69 68 ralrimivvva ⊢ φ → ∀ x ∈ Base Scalar ⁡ U ∀ a ∈ Q ∀ b ∈ Q x ⋅ U a + U b ∈ Q
70 62 63 18 54 64 4 islss ⊢ Q ∈ S ↔ Q ⊆ Base U ∧ Q ≠ ∅ ∧ ∀ x ∈ Base Scalar ⁡ U ∀ a ∈ Q ∀ b ∈ Q x ⋅ U a + U b ∈ Q
71 33 53 69 70 syl3anbrc ⊢ φ → Q ∈ S