Metamath Proof Explorer

Theorem lkrss2N

Description: Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lkrss2.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
2 lkrss2.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
3 lkrss2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lkrss2.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
5 lkrss2.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
6 lkrss2.t ⊢ · = ( ·𝑠 ‘ 𝐷 )
7 lkrss2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lkrss2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 lkrss2.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
10 sspss ⊢ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ↔ ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ∨ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) )
11 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
12 3 4 5 11 7 8 9 lkrpssN ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ↔ ( 𝐺 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) ) )
13 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14 7 13 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
15 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
16 1 2 15 lmod0cl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
17 14 16 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → 𝐻 = ( 0g ‘ 𝐷 ) )
20 3 1 15 5 6 11 14 8 ldual0vs ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) · 𝐺 ) = ( 0g ‘ 𝐷 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → ( ( 0g ‘ 𝑆 ) · 𝐺 ) = ( 0g ‘ 𝐷 ) )
22 19 21 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → 𝐻 = ( ( 0g ‘ 𝑆 ) · 𝐺 ) )
23 oveq1 ⊢ ( 𝑟 = ( 0g ‘ 𝑆 ) → ( 𝑟 · 𝐺 ) = ( ( 0g ‘ 𝑆 ) · 𝐺 ) )
24 23 rspceeqv ⊢ ( ( ( 0g ‘ 𝑆 ) ∈ 𝑅 ∧ 𝐻 = ( ( 0g ‘ 𝑆 ) · 𝐺 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
25 18 22 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
26 25 ex ⊢ ( 𝜑 → ( 𝐻 = ( 0g ‘ 𝐷 ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) )
27 26 adantld ⊢ ( 𝜑 → ( ( 𝐺 ≠ ( 0g ‘ 𝐷 ) ∧ 𝐻 = ( 0g ‘ 𝐷 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) )
28 12 27 sylbid ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) )
29 28 imp ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
30 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → 𝑊 ∈ LVec )
31 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → 𝐺 ∈ 𝐹 )
32 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → 𝐻 ∈ 𝐹 )
33 simpr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
34 1 2 3 4 5 6 30 31 32 33 eqlkr4 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
35 29 34 jaodan ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ∨ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
36 10 35 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) )
37 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑊 ∈ LVec )
38 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐺 ∈ 𝐹 )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ 𝑅 )
40 1 2 3 4 5 6 37 38 39 lkrss ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ ( 𝑟 · 𝐺 ) ) )
41 40 ex ⊢ ( 𝜑 → ( 𝑟 ∈ 𝑅 → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ ( 𝑟 · 𝐺 ) ) ) )
42 fveq2 ⊢ ( 𝐻 = ( 𝑟 · 𝐺 ) → ( 𝐾 ‘ 𝐻 ) = ( 𝐾 ‘ ( 𝑟 · 𝐺 ) ) )
43 42 sseq2d ⊢ ( 𝐻 = ( 𝑟 · 𝐺 ) → ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ↔ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ ( 𝑟 · 𝐺 ) ) ) )
44 43 biimprcd ⊢ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ ( 𝑟 · 𝐺 ) ) → ( 𝐻 = ( 𝑟 · 𝐺 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) )
45 41 44 syl6 ⊢ ( 𝜑 → ( 𝑟 ∈ 𝑅 → ( 𝐻 = ( 𝑟 · 𝐺 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ) )
46 45 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) )
47 46 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) )
48 36 47 impbida ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ↔ ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) )