Metamath Proof Explorer

Theorem lfl1dim2N

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim may be more compatible with lspsn . (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lfl1dim.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfl1dim.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lfl1dim.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfl1dim.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
lfl1dim.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lfl1dim.t ⊢ · = ( .r ‘ 𝐷 )
lfl1dim.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lfl1dim.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lfl1dim2N ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∈ 𝐹 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } )

Proof

Step Hyp Ref Expression
1 lfl1dim.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lfl1dim.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lfl1dim.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lfl1dim.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
5 lfl1dim.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
6 lfl1dim.t ⊢ · = ( .r ‘ 𝐷 )
7 lfl1dim.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lfl1dim.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 7 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
12 2 5 11 lmod0cl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
13 10 12 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
15 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
16 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑊 ∈ LMod )
17 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝐺 ∈ 𝐹 )
18 1 2 3 5 6 11 16 17 lfl0sc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
19 15 18 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
20 sneq ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → { 𝑘 } = { ( 0g ‘ 𝐷 ) } )
21 20 xpeq2d ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
22 21 oveq2d ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
23 22 rspceeqv ⊢ ( ( ( 0g ‘ 𝐷 ) ∈ 𝐾 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
24 14 19 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
25 24 a1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
26 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
27 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LMod )
28 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
29 1 3 4 27 28 lkrssv ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 )
30 10 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑊 ∈ LMod )
31 8 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝐺 ∈ 𝐹 )
32 2 11 1 3 4 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
33 30 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
34 33 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
35 34 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) ) )
36 35 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) )
37 29 36 eqssd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) = 𝑉 )
38 2 11 1 3 4 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
39 27 28 38 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
40 37 39 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
41 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
42 1 2 3 5 6 11 27 41 lfl0sc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
43 40 42 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
44 26 43 23 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
45 44 ex ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
46 eqid ⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
47 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑊 ∈ LVec )
48 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ∈ 𝐹 )
49 simprr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
50 1 2 11 46 3 4 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
51 47 48 49 50 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
52 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ∈ 𝐹 )
53 simprl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
54 1 2 11 46 3 4 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
55 47 52 53 54 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
56 46 47 51 55 lshpcmp ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) )
57 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LVec )
58 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
59 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
60 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) )
61 2 5 6 1 3 4 eqlkr2 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
62 57 58 59 60 61 syl121anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
63 62 ex ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
64 56 63 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
65 25 45 64 pm2.61da2ne ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
66 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LVec )
67 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 )
68 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 )
69 1 2 5 6 3 4 66 67 68 lkrscss ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
70 69 ex ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
71 fveq2 ⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
72 71 sseq2d ⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
73 72 biimprcd ⊢ ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
74 70 73 syl6 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) )
75 74 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
76 65 75 impbid ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
77 76 rabbidva ⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∈ 𝐹 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } )