Theorem lkreqN

Description: Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lkreq.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	lkreq.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lkreq.o	⊢ 0 = ( 0g ‘ 𝑆 )
	lkreq.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkreq.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkreq.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	lkreq.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lkreq.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lkreq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
	lkreq.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
	lkreq.g	⊢ ( 𝜑 → 𝐺 = ( 𝐴 · 𝐻 ) )
Assertion	lkreqN	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		lkreq.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
2		lkreq.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
3		lkreq.o	⊢ 0 = ( 0g ‘ 𝑆 )
4		lkreq.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		lkreq.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
6		lkreq.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
7		lkreq.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
8		lkreq.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
9		lkreq.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
10		lkreq.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
11		lkreq.g	⊢ ( 𝜑 → 𝐺 = ( 𝐴 · 𝐻 ) )
12	11	eqeq1d	⊢ ( 𝜑 → ( 𝐺 = ( 0g ‘ 𝐷 ) ↔ ( 𝐴 · 𝐻 ) = ( 0g ‘ 𝐷 ) ) )
13		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
15		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
16		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
17		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
18	6 8	lduallvec	⊢ ( 𝜑 → 𝐷 ∈ LVec )
19	9	eldifad	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
20	1 2 6 14 15 8	ldualsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = 𝑅 )
21	19 20	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
22	4 6 13 8 10	ldualelvbase	⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝐷 ) )
23	13 7 14 15 16 17 18 21 22	lvecvs0or	⊢ ( 𝜑 → ( ( 𝐴 · 𝐻 ) = ( 0g ‘ 𝐷 ) ↔ ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = ( 0g ‘ 𝐷 ) ) ) )
24		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25	8 24	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
26	1 3 6 14 16 25	ldual0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = 0 )
27	26	eqeq2d	⊢ ( 𝜑 → ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ↔ 𝐴 = 0 ) )
28		eldifsni	⊢ ( 𝐴 ∈ ( 𝑅 ∖ { 0 } ) → 𝐴 ≠ 0 )
29	9 28	syl	⊢ ( 𝜑 → 𝐴 ≠ 0 )
30	29	a1d	⊢ ( 𝜑 → ( 𝐻 ≠ ( 0g ‘ 𝐷 ) → 𝐴 ≠ 0 ) )
31	30	necon4d	⊢ ( 𝜑 → ( 𝐴 = 0 → 𝐻 = ( 0g ‘ 𝐷 ) ) )
32	27 31	sylbid	⊢ ( 𝜑 → ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) → 𝐻 = ( 0g ‘ 𝐷 ) ) )
33		idd	⊢ ( 𝜑 → ( 𝐻 = ( 0g ‘ 𝐷 ) → 𝐻 = ( 0g ‘ 𝐷 ) ) )
34	32 33	jaod	⊢ ( 𝜑 → ( ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = ( 0g ‘ 𝐷 ) ) → 𝐻 = ( 0g ‘ 𝐷 ) ) )
35	23 34	sylbid	⊢ ( 𝜑 → ( ( 𝐴 · 𝐻 ) = ( 0g ‘ 𝐷 ) → 𝐻 = ( 0g ‘ 𝐷 ) ) )
36	12 35	sylbid	⊢ ( 𝜑 → ( 𝐺 = ( 0g ‘ 𝐷 ) → 𝐻 = ( 0g ‘ 𝐷 ) ) )
37		nne	⊢ ( ¬ 𝐻 ≠ ( 0g ‘ 𝐷 ) ↔ 𝐻 = ( 0g ‘ 𝐷 ) )
38	36 37	imbitrrdi	⊢ ( 𝜑 → ( 𝐺 = ( 0g ‘ 𝐷 ) → ¬ 𝐻 ≠ ( 0g ‘ 𝐷 ) ) )
39	38	con3d	⊢ ( 𝜑 → ( ¬ ¬ 𝐻 ≠ ( 0g ‘ 𝐷 ) → ¬ 𝐺 = ( 0g ‘ 𝐷 ) ) )
40	39	orrd	⊢ ( 𝜑 → ( ¬ 𝐻 ≠ ( 0g ‘ 𝐷 ) ∨ ¬ 𝐺 = ( 0g ‘ 𝐷 ) ) )
41		ianor	⊢ ( ¬ ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) ↔ ( ¬ 𝐻 ≠ ( 0g ‘ 𝐷 ) ∨ ¬ 𝐺 = ( 0g ‘ 𝐷 ) ) )
42	40 41	sylibr	⊢ ( 𝜑 → ¬ ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) )
43	4 1 2 6 7 25 19 10	ldualvscl	⊢ ( 𝜑 → ( 𝐴 · 𝐻 ) ∈ 𝐹 )
44	11 43	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
45	4 5 6 17 8 10 44	lkrpssN	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐻 ) ⊊ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) ) )
46		df-pss	⊢ ( ( 𝐾 ‘ 𝐻 ) ⊊ ( 𝐾 ‘ 𝐺 ) ↔ ( ( 𝐾 ‘ 𝐻 ) ⊆ ( 𝐾 ‘ 𝐺 ) ∧ ( 𝐾 ‘ 𝐻 ) ≠ ( 𝐾 ‘ 𝐺 ) ) )
47	45 46	bitr3di	⊢ ( 𝜑 → ( ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) ↔ ( ( 𝐾 ‘ 𝐻 ) ⊆ ( 𝐾 ‘ 𝐺 ) ∧ ( 𝐾 ‘ 𝐻 ) ≠ ( 𝐾 ‘ 𝐺 ) ) ) )
48	1 2 4 5 6 7 8 10 19	lkrss	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐻 ) ⊆ ( 𝐾 ‘ ( 𝐴 · 𝐻 ) ) )
49	11	fveq2d	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ ( 𝐴 · 𝐻 ) ) )
50	48 49	sseqtrrd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐻 ) ⊆ ( 𝐾 ‘ 𝐺 ) )
51	50	biantrurd	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐻 ) ≠ ( 𝐾 ‘ 𝐺 ) ↔ ( ( 𝐾 ‘ 𝐻 ) ⊆ ( 𝐾 ‘ 𝐺 ) ∧ ( 𝐾 ‘ 𝐻 ) ≠ ( 𝐾 ‘ 𝐺 ) ) ) )
52	47 51	bitr4d	⊢ ( 𝜑 → ( ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) ↔ ( 𝐾 ‘ 𝐻 ) ≠ ( 𝐾 ‘ 𝐺 ) ) )
53	52	necon2bbid	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐻 ) = ( 𝐾 ‘ 𝐺 ) ↔ ¬ ( 𝐻 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐺 = ( 0g ‘ 𝐷 ) ) ) )
54	42 53	mpbird	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐻 ) = ( 𝐾 ‘ 𝐺 ) )
55	54	eqcomd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )