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 lspsnel5 ( ( ( ( ( 𝜑𝑓𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ∈ ( 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 lspsnel5a ( ( ( 𝜑𝑓𝐶 ) ∧ 𝑣𝑇 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 )
58 53 57 eqsstrd ( ( ( 𝜑𝑓𝐶 ) ∧ 𝑣𝑇 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 )
59 58 rexlimdv3a ( ( 𝜑𝑓𝐶 ) → ( ∃ 𝑣𝑇 ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) → ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) )
60 52 59 impbid ( ( 𝜑𝑓𝐶 ) → ( ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ↔ ∃ 𝑣𝑇 ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) )
61 60 rabbidva ( 𝜑 → { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 } = { 𝑓𝐶 ∣ ∃ 𝑣𝑇 ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } )
62 12 61 eqtrd ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐶 ∣ ∃ 𝑣𝑇 ( 𝑂 ‘ ( 𝐿𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } )