Theorem lkrscss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (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	⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
Assertion	lkrscss	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘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		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	7 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	1 5 6 11 8	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
13		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
14	1 2 5 3 4 13 11 8	lfl0sc	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
15	14	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) = ( 𝐿 ‘ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
16		eqid	⊢ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } )
17	2 13 1 5	lfl0f	⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∈ 𝐹 )
18	2 13 1 5 6	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∈ 𝐹 ) → ( ( 𝐿 ‘ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = 𝑉 ↔ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
19	11 17 18	syl2anc2	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = 𝑉 ↔ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
20	16 19	mpbiri	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = 𝑉 )
21	15 20	eqtr2d	⊢ ( 𝜑 → 𝑉 = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) )
22	12 21	sseqtrd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑅 = ( 0g ‘ 𝐷 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) )
24		sneq	⊢ ( 𝑅 = ( 0g ‘ 𝐷 ) → { 𝑅 } = { ( 0g ‘ 𝐷 ) } )
25	24	xpeq2d	⊢ ( 𝑅 = ( 0g ‘ 𝐷 ) → ( 𝑉 × { 𝑅 } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) )
26	25	oveq2d	⊢ ( 𝑅 = ( 0g ‘ 𝐷 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) )
27	26	fveq2d	⊢ ( 𝑅 = ( 0g ‘ 𝐷 ) → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑅 = ( 0g ‘ 𝐷 ) ) → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) )
29	23 28	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝑅 = ( 0g ‘ 𝐷 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) )
30	7	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → 𝑊 ∈ LVec )
31	8	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → 𝐺 ∈ 𝐹 )
32	9	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → 𝑅 ∈ 𝐾 )
33		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → 𝑅 ≠ ( 0g ‘ 𝐷 ) )
34	1 2 3 4 5 6 30 31 32 13 33	lkrsc	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) )
35		eqimss2	⊢ ( ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) )
36	34 35	syl	⊢ ( ( 𝜑 ∧ 𝑅 ≠ ( 0g ‘ 𝐷 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) )
37	29 36	pm2.61dane	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) )