Metamath Proof Explorer

Theorem mapdsn

Description: Value of the map defined by df-mapd at the span of a singleton. (Contributed by NM, 16-Feb-2015)

Ref Expression
Hypotheses mapdsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdsn.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdsn.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdsn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdsn.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdsn.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdsn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion mapdsn ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) } )

Proof

Step Hyp Ref Expression
1 mapdsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdsn.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdsn.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4 mapdsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 mapdsn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 mapdsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7 mapdsn.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
8 mapdsn.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
9 mapdsn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 mapdsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
12 1 4 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 5 11 6 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
14 12 10 13 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
15 1 4 11 7 8 2 3 9 14 mapdval ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) } )
16 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 10 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
18 5 6 lspssv ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 )
19 12 17 18 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 )
21 simprr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
22 1 4 5 2 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑂 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
23 16 20 21 22 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑂 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ⊆ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
24 1 4 2 5 6 9 17 dochocsp ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑂 ‘ { 𝑋 } ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑂 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑂 ‘ { 𝑋 } ) )
26 simprl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) )
27 23 25 26 3sstr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) )
28 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → 𝑓 ∈ 𝐹 )
30 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → 𝑋 ∈ 𝑉 )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) )
32 1 2 4 5 7 8 28 29 30 31 lcfl9a ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) )
33 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → 𝑈 ∈ LMod )
34 5 7 8 33 29 lkrssv ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 )
35 1 4 5 2 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑂 ‘ ( 𝑂 ‘ { 𝑋 } ) ) )
36 28 34 31 35 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑂 ‘ ( 𝑂 ‘ { 𝑋 } ) ) )
37 1 4 2 5 6 9 10 dochocsn ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
39 36 38 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
40 32 39 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) )
41 27 40 impbida ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) → ( ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) ↔ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) ) )
42 41 rabbidva ⊢ ( 𝜑 → { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) } = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) } )
43 15 42 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝑓 ) } )