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	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ↔ ∃ 𝑟 ∈ 𝑅 𝐻 = ( 𝑟 · 𝐺 ) ) )