Step |
Hyp |
Ref |
Expression |
1 |
|
lflf.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
2 |
|
lflf.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
3 |
|
lflf.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
4 |
|
lflf.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
6 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) |
8 |
|
eqid |
⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 ) |
9 |
3 5 1 6 2 7 8 4
|
islfl |
⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) ) ) ) |
10 |
9
|
simprbda |
⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 ) |