Metamath Proof Explorer

Theorem mapdval2N

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdval2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdval2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdval2.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdval2.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdval2.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdval2.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdval2.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdval2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdval2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
mapdval2.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
Assertion mapdval2N ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } )

Proof

Step Hyp Ref Expression
1 mapdval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdval2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdval2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdval2.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 mapdval2.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 mapdval2.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 mapdval2.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
8 mapdval2.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
9 mapdval2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 mapdval2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
11 mapdval2.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
12 1 2 3 5 6 7 8 9 10 11 mapdvalc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } )
13 1 2 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
14 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → 𝑈 ∈ LMod )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
16 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
17 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
18 16 4 17 islsati ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
19 14 15 18 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
20 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
21 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 )
22 20 21 eqsstrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 )
23 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑈 ∈ LMod )
24 23 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑈 ∈ LMod )
25 10 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑇 ∈ 𝑆 )
26 25 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑇 ∈ 𝑆 )
27 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
28 16 3 4 24 26 27 ellspsn5b ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑣 ∈ 𝑇 ↔ ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 ) )
29 22 28 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑣 ∈ 𝑇 )
30 19 29 20 reximssdv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
31 30 ex ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) )
32 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
33 32 3 lss0cl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → ( 0g ‘ 𝑈 ) ∈ 𝑇 )
34 13 10 33 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑇 )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 0g ‘ 𝑈 ) ∈ 𝑇 )
36 simpr ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } )
37 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → 𝑈 ∈ LMod )
38 32 4 lspsn0 ⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
40 36 39 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
41 sneq ⊢ ( 𝑣 = ( 0g ‘ 𝑈 ) → { 𝑣 } = { ( 0g ‘ 𝑈 ) } )
42 41 fveq2d ⊢ ( 𝑣 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑣 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
43 42 rspceeqv ⊢ ( ( ( 0g ‘ 𝑈 ) ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
44 35 40 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
46 45 a1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) )
47 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
48 11 lcfl1lem ⊢ ( 𝑓 ∈ 𝐶 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) )
49 48 simplbi ⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ∈ 𝐹 )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ 𝐹 )
51 1 7 2 32 17 5 6 47 50 dochsat0 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) )
52 31 46 51 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) )
53 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) )
54 23 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑈 ∈ LMod )
55 25 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑇 ∈ 𝑆 )
56 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑣 ∈ 𝑇 )
57 3 4 54 55 56 ellspsn5 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 )
58 53 57 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 )
59 58 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) )
60 52 59 impbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ↔ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) )
61 60 rabbidva ⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } = { 𝑓 ∈ 𝐶 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } )
62 12 61 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } )