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 · ( 𝑉 × { 𝑘 } ) ) } )