Metamath Proof Explorer

Theorem lfl1dim

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014)

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 lfl1dim ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘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 df-rab ⊢ { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) }
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 7 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
13 2 5 12 lmod0cl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
14 11 13 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
17 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑊 ∈ LMod )
18 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝐺 ∈ 𝐹 )
19 1 2 3 5 6 12 17 18 lfl0sc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
20 16 19 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
21 sneq ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → { 𝑘 } = { ( 0g ‘ 𝐷 ) } )
22 21 xpeq2d ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
23 22 oveq2d ⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
24 23 rspceeqv ⊢ ( ( ( 0g ‘ 𝐷 ) ∈ 𝐾 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
25 15 20 24 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
26 25 a1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
27 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 )
28 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LMod )
29 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
30 1 3 4 28 29 lkrssv ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 )
31 11 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑊 ∈ LMod )
32 8 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝐺 ∈ 𝐹 )
33 2 12 1 3 4 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
34 31 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
35 34 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
36 35 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) ) )
37 36 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) )
38 30 37 eqssd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) = 𝑉 )
39 2 12 1 3 4 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
40 28 29 39 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
41 38 40 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
42 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
43 1 2 3 5 6 12 28 42 lfl0sc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
44 41 43 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
45 27 44 24 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
46 45 ex ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
47 eqid ⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
48 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑊 ∈ LVec )
49 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ∈ 𝐹 )
50 simprr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
51 1 2 12 47 3 4 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
52 48 49 50 51 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ∈ 𝐹 )
54 simprl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
55 1 2 12 47 3 4 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
56 48 53 54 55 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) )
57 47 48 52 56 lshpcmp ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) )
58 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LVec )
59 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 )
60 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 )
61 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) )
62 2 5 6 1 3 4 eqlkr2 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
63 58 59 60 61 62 syl121anc ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) )
64 63 ex ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
65 57 64 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
66 26 46 65 pm2.61da2ne ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
67 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LVec )
68 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 )
70 1 2 5 6 3 4 67 68 69 lkrscss ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
71 70 ex ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
72 fveq2 ⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
73 72 sseq2d ⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
74 73 biimprcd ⊢ ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
75 71 74 syl6 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) )
76 75 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) )
77 66 76 impbid ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
78 77 pm5.32da ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
79 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LMod )
80 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 )
82 1 2 5 6 3 79 80 81 lflvscl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ∈ 𝐹 )
83 eleq1a ⊢ ( ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ∈ 𝐹 → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → 𝑔 ∈ 𝐹 ) )
84 82 83 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → 𝑔 ∈ 𝐹 ) )
85 84 pm4.71rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
86 85 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ↔ ∃ 𝑘 ∈ 𝐾 ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) )
87 r19.42v ⊢ ( ∃ 𝑘 ∈ 𝐾 ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
88 86 87 bitr2di ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
89 78 88 bitrd ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) )
90 89 abbidv ⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } )
91 9 90 syl5eq ⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } )