Metamath Proof Explorer

Theorem mapdval4N

Description: Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is C_ C ) 2. The unneeded direction of lcfl8a has awkward E. - add another thm with only one direction of it? 3. Swap O{ v } and Lf ? (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mapdval4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdval4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdval4.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdval4.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5 mapdval4.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
6 mapdval4.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 mapdval4.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 mapdval4.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 mapdval4.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
10 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
11 eqid ⊢ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
12 1 2 3 10 4 5 6 7 8 9 11 mapdval2N ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) } )
13 11 lcfl1lem ⊢ ( 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) )
14 13 anbi1i ⊢ ( ( 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
15 anass ⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( 𝑓 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
16 14 15 bitri ⊢ ( ( 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( 𝑓 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) )
17 r19.42v ⊢ ( ∃ 𝑣 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
18 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
19 18 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
20 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) )
21 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
22 8 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24 23 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) → 𝑇 ∈ 𝑆 )
26 21 3 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
27 25 26 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
28 27 snssd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) → { 𝑣 } ⊆ ( Base ‘ 𝑈 ) )
29 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → { 𝑣 } ⊆ ( Base ‘ 𝑈 ) )
30 1 2 6 21 10 24 29 dochocsp ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( 𝑂 ‘ { 𝑣 } ) )
31 19 20 30 3eqtr3rd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) )
32 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
33 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) )
34 33 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ { 𝑣 } ) )
35 sneq ⊢ ( 𝑤 = 𝑣 → { 𝑤 } = { 𝑣 } )
36 35 fveq2d ⊢ ( 𝑤 = 𝑣 → ( 𝑂 ‘ { 𝑤 } ) = ( 𝑂 ‘ { 𝑣 } ) )
37 36 rspceeqv ⊢ ( ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ { 𝑣 } ) ) → ∃ 𝑤 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ { 𝑤 } ) )
38 32 34 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ∃ 𝑤 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ { 𝑤 } ) )
39 23 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
40 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → 𝑓 ∈ 𝐹 )
41 1 6 2 21 4 5 39 40 lcfl8a ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ↔ ∃ 𝑤 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ { 𝑤 } ) ) )
42 38 41 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) )
43 1 2 6 21 10 23 27 dochocsn ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝑂 ‘ { 𝑣 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
44 fveq2 ⊢ ( ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) → ( 𝑂 ‘ ( 𝑂 ‘ { 𝑣 } ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
45 43 44 sylan9req ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
46 45 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
47 42 46 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) ∧ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
48 31 47 impbida ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑇 ) → ( ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) )
49 48 rexbidva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) → ( ∃ 𝑣 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) )
50 17 49 bitr3id ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐹 ) → ( ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) )
51 50 pm5.32da ⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) ↔ ( 𝑓 ∈ 𝐹 ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) ) )
52 16 51 syl5bb ⊢ ( 𝜑 → ( ( 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ↔ ( 𝑓 ∈ 𝐹 ∧ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) ) ) )
53 52 rabbidva2 ⊢ ( 𝜑 → { 𝑓 ∈ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) } = { 𝑓 ∈ 𝐹 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) } )
54 12 53 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿 ‘ 𝑓 ) } )