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 ⊢ 𝐻 = ( 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 syl5bi ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑅 → ( 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
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 syl5bb ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
62 61 eqrdv ⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
63 10 62 syl5eq ⊢ ( 𝜑 → 𝑄 = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )