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 · ( 𝑉 × { 𝑟 } ) ) )