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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrvalsn.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrvalsn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrvalsn.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfrvalsn.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrvalsn.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrvalsn.n	⊢ 𝑁 = ( LSpan ‘ 𝐷 )
	lcfrvalsn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrvalsn.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcfrvalsn.q	⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) )
	lcfrvalsn.r	⊢ 𝑅 = ( 𝑁 ‘ { 𝐺 } )
Assertion	lcfrvalsnN	⊢ ( 𝜑 → 𝑄 = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfrvalsn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrvalsn.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrvalsn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrvalsn.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5		lcfrvalsn.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
6		lcfrvalsn.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lcfrvalsn.n	⊢ 𝑁 = ( LSpan ‘ 𝐷 )
8		lcfrvalsn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		lcfrvalsn.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10		lcfrvalsn.q	⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) )
11		lcfrvalsn.r	⊢ 𝑅 = ( 𝑁 ‘ { 𝐺 } )
12		eliun	⊢ ( 𝑥 ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
13	11	eleq2i	⊢ ( 𝑓 ∈ 𝑅 ↔ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) )
14	8	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
16	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝑈 ∈ LMod )
18	6 16	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
19		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
20	4 6 19 16 9	ldualelvbase	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
21		eqid	⊢ ( LSubSp ‘ 𝐷 ) = ( LSubSp ‘ 𝐷 )
22	19 21 7	lspsncl	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑁 ‘ { 𝐺 } ) ∈ ( LSubSp ‘ 𝐷 ) )
23	18 20 22	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) ∈ ( LSubSp ‘ 𝐷 ) )
24	19 21	lssel	⊢ ( ( ( 𝑁 ‘ { 𝐺 } ) ∈ ( LSubSp ‘ 𝐷 ) ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝑓 ∈ ( Base ‘ 𝐷 ) )
25	23 24	sylan	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝑓 ∈ ( Base ‘ 𝐷 ) )
26	4 6 19 16	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( Base ‘ 𝐷 ) = 𝐹 )
28	25 27	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝑓 ∈ 𝐹 )
29	15 4 5 17 28	lkrssv	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( 𝐿 ‘ 𝑓 ) ⊆ ( Base ‘ 𝑈 ) )
30		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
31		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
32		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
33	30 31 19 32 7	lspsnel	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) )
34	18 20 33	syl2anc	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) )
35		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
36		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
37	35 36 6 30 31 16	ldualsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
38	37	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) )
39	34 38	bitrd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) )
40	39	biimpa	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) )
41	1 3 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝑈 ∈ LVec )
43	9	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → 𝐺 ∈ 𝐹 )
44	35 36 4 5 6 32 42 43 28	lkrss2N	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑓 ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) )
45	40 44	mpbird	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑓 ) )
46	1 3 15 2	dochss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑓 ) ⊆ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
47	14 29 45 46	syl3anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
48	47	sseld	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) ) → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
49	48	ex	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑁 ‘ { 𝐺 } ) → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
50	13 49	biimtrid	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑅 → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
51	50	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
52	19 7	lspsnid	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → 𝐺 ∈ ( 𝑁 ‘ { 𝐺 } ) )
53	18 20 52	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ‘ { 𝐺 } ) )
54	53 11	eleqtrrdi	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
55		2fveq3	⊢ ( 𝑓 = 𝐺 → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
56	55	eleq2d	⊢ ( 𝑓 = 𝐺 → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
57	56	rspcev	⊢ ( ( 𝐺 ∈ 𝑅 ∧ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
58	54 57	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
59	58	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) → ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
60	51 59	impbid	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝑅 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
61	12 60	bitrid	⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
62	61	eqrdv	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
63	10 62	eqtrid	⊢ ( 𝜑 → 𝑄 = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )