eqlkr4

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	eqlkr4.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	eqlkr4.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	eqlkr4.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	eqlkr4.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	eqlkr4.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	eqlkr4.t	⊢ · = ( ·_𝑠 ‘ 𝐷 )
	eqlkr4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	eqlkr4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	eqlkr4.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
	eqlkr4.e	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
Assertion	eqlkr4	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqlkr4.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
2		eqlkr4.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
3		eqlkr4.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		eqlkr4.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
5		eqlkr4.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
6		eqlkr4.t	⊢ · = ( ·_𝑠 ‘ 𝐷 )
7		eqlkr4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		eqlkr4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		eqlkr4.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
10		eqlkr4.e	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
11		eqid	⊢ ( ._r ‘ 𝑆 ) = ( ._r ‘ 𝑆 )
12		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13	1 2 11 12 3 4	eqlkr2	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝐺 ∘_f ( ._r ‘ 𝑆 ) ( ( Base ‘ 𝑊 ) × { 𝑟 } ) ) )
14	7 8 9 10 13	syl121anc	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝐺 ∘_f ( ._r ‘ 𝑆 ) ( ( Base ‘ 𝑊 ) × { 𝑟 } ) ) )
15	7	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑊 ∈ LVec )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ 𝑅 )
17	8	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐺 ∈ 𝐹 )
18	3 12 1 2 11 5 6 15 16 17	ldualvs	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 · 𝐺 ) = ( 𝐺 ∘_f ( ._r ‘ 𝑆 ) ( ( Base ‘ 𝑊 ) × { 𝑟 } ) ) )
19	18	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐻 = ( 𝑟 · 𝐺 ) ↔ 𝐻 = ( 𝐺 ∘_f ( ._r ‘ 𝑆 ) ( ( Base ‘ 𝑊 ) × { 𝑟 } ) ) ) )
20	19	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ↔ ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝐺 ∘_f ( ._r ‘ 𝑆 ) ( ( Base ‘ 𝑊 ) × { 𝑟 } ) ) ) )
21	14 20	mpbird	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )

Metamath Proof Explorer

Theorem eqlkr4

Proof