This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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