Metamath Proof Explorer

Definition df-mapd

Description: Extend class notation with a one-to-one onto ( mapd1o ), order-preserving ( mapdord ) map, called a projectivity (definition of projectivity in Baer p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015)

Ref Expression
Assertion df-mapd mapd = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpd ⊢ mapd
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vs ⊢ 𝑠
8 clss ⊢ LSubSp
9 cdvh ⊢ DVecH
10 5 9 cfv ⊢ ( DVecH ‘ 𝑘 )
11 3 cv ⊢ 𝑤
12 11 10 cfv ⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
13 12 8 cfv ⊢ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
14 vf ⊢ 𝑓
15 clfn ⊢ LFnl
16 12 15 cfv ⊢ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
17 coch ⊢ ocH
18 5 17 cfv ⊢ ( ocH ‘ 𝑘 )
19 11 18 cfv ⊢ ( ( ocH ‘ 𝑘 ) ‘ 𝑤 )
20 clk ⊢ LKer
21 12 20 cfv ⊢ ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
22 14 cv ⊢ 𝑓
23 22 21 cfv ⊢ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 )
24 23 19 cfv ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) )
25 24 19 cfv ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) )
26 25 23 wceq ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 )
27 7 cv ⊢ 𝑠
28 24 27 wss ⊢ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠
29 26 28 wa ⊢ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 )
30 29 14 16 crab ⊢ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) }
31 7 13 30 cmpt ⊢ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } )
32 3 6 31 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )
33 1 2 32 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )
34 0 33 wceq ⊢ mapd = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )