Step |
Hyp |
Ref |
Expression |
1 |
|
lkrfval2.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lkrfval2.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
3 |
|
lkrfval2.o |
⊢ 0 = ( 0g ‘ 𝐷 ) |
4 |
|
lkrfval2.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
5 |
|
lkrfval2.k |
⊢ 𝐾 = ( LKer ‘ 𝑊 ) |
6 |
|
elex |
⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V ) |
7 |
1 2 3 4 5
|
ellkr |
⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) ) |
8 |
7
|
abbi2dv |
⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) } ) |
9 |
|
df-rab |
⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) } |
10 |
8 9
|
eqtr4di |
⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } ) |
11 |
6 10
|
sylan |
⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } ) |