Step |
Hyp |
Ref |
Expression |
1 |
|
lflset.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lflset.a |
⊢ + = ( +g ‘ 𝑊 ) |
3 |
|
lflset.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
4 |
|
lflset.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
5 |
|
lflset.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
6 |
|
lflset.p |
⊢ ⨣ = ( +g ‘ 𝐷 ) |
7 |
|
lflset.t |
⊢ × = ( .r ‘ 𝐷 ) |
8 |
|
lflset.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
9 |
1 2 3 4 5 6 7 8
|
lflset |
⊢ ( 𝑊 ∈ 𝑋 → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ) |
10 |
9
|
eleq2d |
⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ 𝐹 ↔ 𝐺 ∈ { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ) ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) ) |
12 |
|
fveq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
13 |
12
|
oveq2d |
⊢ ( 𝑓 = 𝐺 → ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) = ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ) |
14 |
|
fveq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
15 |
13 14
|
oveq12d |
⊢ ( 𝑓 = 𝐺 → ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) |
16 |
11 15
|
eqeq12d |
⊢ ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
17 |
16
|
2ralbidv |
⊢ ( 𝑓 = 𝐺 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
18 |
17
|
ralbidv |
⊢ ( 𝑓 = 𝐺 → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
19 |
18
|
elrab |
⊢ ( 𝐺 ∈ { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ↔ ( 𝐺 ∈ ( 𝐾 ↑m 𝑉 ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
20 |
5
|
fvexi |
⊢ 𝐾 ∈ V |
21 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
22 |
20 21
|
elmap |
⊢ ( 𝐺 ∈ ( 𝐾 ↑m 𝑉 ) ↔ 𝐺 : 𝑉 ⟶ 𝐾 ) |
23 |
22
|
anbi1i |
⊢ ( ( 𝐺 ∈ ( 𝐾 ↑m 𝑉 ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
24 |
19 23
|
bitri |
⊢ ( 𝐺 ∈ { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
25 |
10 24
|
bitrdi |
⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) ) |