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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfr.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	lcfr.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfr.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfr.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfr.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	lcfr.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcfr.q	⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfr.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
	lcfr.rs	⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
Assertion	lcfr	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lcfr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfr.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		lcfr.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcfr.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcfr.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfr.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
9		lcfr.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
10		lcfr.q	⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
11		lcfr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		lcfr.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
13		lcfr.rs	⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
14		2fveq3	⊢ ( 𝑔 = ℎ → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) = ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
15	14	cbviunv	⊢ ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) = ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) )
16	10 15	eqtri	⊢ 𝑄 = ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) )
17	11	adantr	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑅 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
19	1 3 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20	19	adantr	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑅 ) → 𝑈 ∈ LMod )
21		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
22	21 8	lssss	⊢ ( 𝑅 ∈ 𝑇 → 𝑅 ⊆ ( Base ‘ 𝐷 ) )
23	12 22	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝐷 ) )
24	5 7 21 19	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
25	23 24	sseqtrd	⊢ ( 𝜑 → 𝑅 ⊆ 𝐹 )
26	25	sselda	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝐹 )
27	18 5 6 20 26	lkrssv	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑅 ) → ( 𝐿 ‘ ℎ ) ⊆ ( Base ‘ 𝑈 ) )
28	1 3 18 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ℎ ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) )
29	17 27 28	syl2anc	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑅 ) → ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) )
30	29	ralrimiva	⊢ ( 𝜑 → ∀ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) )
31		iunss	⊢ ( ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) ↔ ∀ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) )
32	30 31	sylibr	⊢ ( 𝜑 → ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ⊆ ( Base ‘ 𝑈 ) )
33	16 32	eqsstrid	⊢ ( 𝜑 → 𝑄 ⊆ ( Base ‘ 𝑈 ) )
34	16	a1i	⊢ ( 𝜑 → 𝑄 = ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
35	7 19	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
36		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
37	36 8	lss0cl	⊢ ( ( 𝐷 ∈ LMod ∧ 𝑅 ∈ 𝑇 ) → ( 0g ‘ 𝐷 ) ∈ 𝑅 )
38	35 12 37	syl2anc	⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) ∈ 𝑅 )
39	5 7 36 19	ldual0vcl	⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) ∈ 𝐹 )
40	18 5 6 19 39	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝑈 ) )
41	1 3 18 4 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) ∈ 𝑆 )
42	11 40 41	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) ∈ 𝑆 )
43		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
44	43 4	lss0cl	⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) ∈ 𝑆 ) → ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) )
45	19 42 44	syl2anc	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) )
46		2fveq3	⊢ ( ℎ = ( 0g ‘ 𝐷 ) → ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) = ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) )
47	46	eleq2d	⊢ ( ℎ = ( 0g ‘ 𝐷 ) → ( ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ↔ ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) ) )
48	47	rspcev	⊢ ( ( ( 0g ‘ 𝐷 ) ∈ 𝑅 ∧ ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 0g ‘ 𝐷 ) ) ) ) → ∃ ℎ ∈ 𝑅 ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
49	38 45 48	syl2anc	⊢ ( 𝜑 → ∃ ℎ ∈ 𝑅 ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
50		eliun	⊢ ( ( 0g ‘ 𝑈 ) ∈ ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ↔ ∃ ℎ ∈ 𝑅 ( 0g ‘ 𝑈 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
51	49 50	sylibr	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) )
52	51	ne0d	⊢ ( 𝜑 → ∪ ℎ ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ ℎ ) ) ≠ ∅ )
53	34 52	eqnetrd	⊢ ( 𝜑 → 𝑄 ≠ ∅ )
54		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
55		rabeq	⊢ ( 𝐹 = ( LFnl ‘ 𝑈 ) → { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
56	5 55	ax-mp	⊢ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
57	9 56	eqtri	⊢ 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
58	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
59	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → 𝑅 ∈ 𝑇 )
60	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → 𝑅 ⊆ 𝐶 )
61		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → 𝑎 ∈ 𝑄 )
62		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
63		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
64		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
65		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
66	1 2 3 18 5 6 7 8 58 59 16 61 62 63 64 65	lcfrlem5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ∈ 𝑄 )
67		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → 𝑏 ∈ 𝑄 )
68	1 2 3 54 5 6 7 8 57 16 58 59 60 66 67	lcfrlem42	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) ∈ 𝑄 )
69	68	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∀ 𝑎 ∈ 𝑄 ∀ 𝑏 ∈ 𝑄 ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) ∈ 𝑄 )
70	62 63 18 54 64 4	islss	⊢ ( 𝑄 ∈ 𝑆 ↔ ( 𝑄 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑄 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∀ 𝑎 ∈ 𝑄 ∀ 𝑏 ∈ 𝑄 ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) ∈ 𝑄 ) )
71	33 53 69 70	syl3anbrc	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )