Metamath Proof Explorer


Theorem mapdvalc

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdval.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdval.s 𝑆 = ( LSubSp ‘ 𝑈 )
mapdval.f 𝐹 = ( LFnl ‘ 𝑈 )
mapdval.l 𝐿 = ( LKer ‘ 𝑈 )
mapdval.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdval.k ( 𝜑 → ( 𝐾𝑋𝑊𝐻 ) )
mapdval.t ( 𝜑𝑇𝑆 )
mapdvalc.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
Assertion mapdvalc ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 } )

Proof

Step Hyp Ref Expression
1 mapdval.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdval.s 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdval.f 𝐹 = ( LFnl ‘ 𝑈 )
5 mapdval.l 𝐿 = ( LKer ‘ 𝑈 )
6 mapdval.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 mapdval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 mapdval.k ( 𝜑 → ( 𝐾𝑋𝑊𝐻 ) )
9 mapdval.t ( 𝜑𝑇𝑆 )
10 mapdvalc.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
11 1 2 3 4 5 6 7 8 9 mapdval ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )
12 anass ( ( ( 𝑓𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ) )
13 10 lcfl1lem ( 𝑓𝐶 ↔ ( 𝑓𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ) )
14 13 anbi1i ( ( 𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ↔ ( ( 𝑓𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) )
15 14 bicomi ( ( ( 𝑓𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) )
16 15 a1i ( 𝜑 → ( ( ( 𝑓𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ) )
17 12 16 bitr3id ( 𝜑 → ( ( 𝑓𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ) ↔ ( 𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ) )
18 17 rabbidva2 ( 𝜑 → { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } = { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 } )
19 11 18 eqtrd ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 } )