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

Metamath Proof Explorer

Theorem eqlkr2

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014)

Ref Expression
Hypotheses eqlkr.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
eqlkr.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
eqlkr.t ⊢ · = ( .r ‘ 𝐷 )
eqlkr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
eqlkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
eqlkr.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
Assertion eqlkr2 ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝐾 𝐻 = ( 𝐺 ∘f · ( 𝑉 × { 𝑟 } ) ) )

Proof

Step Hyp Ref Expression
1 eqlkr.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 eqlkr.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
3 eqlkr.t ⊢ · = ( .r ‘ 𝐷 )
4 eqlkr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
5 eqlkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 eqlkr.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
7 1 2 3 4 5 6 eqlkr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑟 ) )
8 4 fvexi ⊢ 𝑉 ∈ V
9 8 a1i ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝑉 ∈ V )
10 simpl1 ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝑊 ∈ LVec )
11 simpl2l ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 )
12 1 2 4 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
13 10 11 12 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
14 13 ffnd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐺 Fn 𝑉 )
15 vex ⊢ 𝑟 ∈ V
16 fnconstg ⊢ ( 𝑟 ∈ V → ( 𝑉 × { 𝑟 } ) Fn 𝑉 )
17 15 16 mp1i ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → ( 𝑉 × { 𝑟 } ) Fn 𝑉 )
18 simpl2r ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐻 ∈ 𝐹 )
19 1 2 4 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : 𝑉 ⟶ 𝐾 )
20 10 18 19 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐻 : 𝑉 ⟶ 𝐾 )
21 20 ffnd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → 𝐻 Fn 𝑉 )
22 eqidd ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
23 15 fvconst2 ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑉 × { 𝑟 } ) ‘ 𝑥 ) = 𝑟 )
24 23 adantl ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑉 × { 𝑟 } ) ‘ 𝑥 ) = 𝑟 )
25 9 14 17 21 22 24 offveqb ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) ∧ 𝑟 ∈ 𝐾 ) → ( 𝐻 = ( 𝐺 ∘f · ( 𝑉 × { 𝑟 } ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑟 ) ) )
26 25 rexbidva ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) → ( ∃ 𝑟 ∈ 𝐾 𝐻 = ( 𝐺 ∘f · ( 𝑉 × { 𝑟 } ) ) ↔ ∃ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑟 ) ) )
27 7 26 mpbird ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝐾 𝐻 = ( 𝐺 ∘f · ( 𝑉 × { 𝑟 } ) ) )