lkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014)

	Ref	Expression
Hypotheses	lkrsc.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrsc.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkrsc.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
	lkrsc.t	⊢ · = ( ._r ‘ 𝐷 )
	lkrsc.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrsc.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
	lkrsc.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lkrsc.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lkrsc.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
	lkrsc.o	⊢ 0 = ( 0_g ‘ 𝐷 )
	lkrsc.e	⊢ ( 𝜑 → 𝑅 ≠ 0 )
Assertion	lkrsc	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		lkrsc.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrsc.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lkrsc.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
4		lkrsc.t	⊢ · = ( ._r ‘ 𝐷 )
5		lkrsc.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6		lkrsc.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
7		lkrsc.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lkrsc.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		lkrsc.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
10		lkrsc.o	⊢ 0 = ( 0_g ‘ 𝐷 )
11		lkrsc.e	⊢ ( 𝜑 → 𝑅 ≠ 0 )
12	1	fvexi	⊢ 𝑉 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
14	2 3 1 5	lflf	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
15	7 8 14	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
16	15	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
17		eqidd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑣 ) )
18	13 9 16 17	ofc2	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) )
19	18	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ↔ ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) = 0 ) )
20	2	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing )
21	7 20	syl	⊢ ( 𝜑 → 𝐷 ∈ DivRing )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐷 ∈ DivRing )
23	7	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LVec )
24	8	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐺 ∈ 𝐹 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
26	2 3 1 5	lflcl	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
27	23 24 25 26	syl3anc	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
28	9	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑅 ∈ 𝐾 )
29	11	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑅 ≠ 0 )
30	3 10 4 22 27 28 29	drngmuleq0	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) = 0 ↔ ( 𝐺 ‘ 𝑣 ) = 0 ) )
31	19 30	bitrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ↔ ( 𝐺 ‘ 𝑣 ) = 0 ) )
32	31	pm5.32da	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
33		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
34	7 33	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
35	1 2 3 4 5 34 8 9	lflvscl	⊢ ( 𝜑 → ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 )
36	1 2 10 5 6	ellkr	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 ) → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ) )
37	7 35 36	syl2anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ) )
38	1 2 10 5 6	ellkr	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
39	7 8 38	syl2anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
40	32 37 39	3bitr4d	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ) ↔ 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ) )
41	40	eqrdv	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐺 ∘_f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem lkrsc

Proof