This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lkrval2

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lkrfval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lkrfval2.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lkrfval2.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrfval2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrfval2.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion lkrval2 ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )

Proof

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 eqabdv ⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) } )
9 df-rab ⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) }
10 8 9 eqtr4di ⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )
11 6 10 sylan ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )