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	$⊢ S = Scalar (W)$
	lkrss2.r	$⊢ R = {Base}_{S}$
	lkrss2.f	$⊢ F = LFnl (W)$
	lkrss2.k	$⊢ K = LKer (W)$
	lkrss2.d	$⊢ D = LDual (W)$
	lkrss2.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lkrss2.w	$⊢ φ \to W \in LVec$
	lkrss2.g	$⊢ φ \to G \in F$
	lkrss2.h	$⊢ φ \to H \in F$
Assertion	lkrss2N	$⊢ φ \to (K (G) \subseteq K (H) \leftrightarrow \exists r \in R H = r \underset{˙}{\cdot} G)$

Proof

Step	Hyp	Ref	Expression
1		lkrss2.s	$⊢ S = Scalar (W)$
2		lkrss2.r	$⊢ R = {Base}_{S}$
3		lkrss2.f	$⊢ F = LFnl (W)$
4		lkrss2.k	$⊢ K = LKer (W)$
5		lkrss2.d	$⊢ D = LDual (W)$
6		lkrss2.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
7		lkrss2.w	$⊢ φ \to W \in LVec$
8		lkrss2.g	$⊢ φ \to G \in F$
9		lkrss2.h	$⊢ φ \to H \in F$
10		sspss	$⊢ K (G) \subseteq K (H) \leftrightarrow (K (G) \subset K (H) \lor K (G) = K (H))$
11		eqid	$⊢ 0_{D} = 0_{D}$
12	3 4 5 11 7 8 9	lkrpssN	$⊢ φ \to (K (G) \subset K (H) \leftrightarrow (G \neq 0_{D} \land H = 0_{D}))$
13		lveclmod	$⊢ W \in LVec \to W \in LMod$
14	7 13	syl	$⊢ φ \to W \in LMod$
15		eqid	$⊢ 0_{S} = 0_{S}$
16	1 2 15	lmod0cl	$⊢ W \in LMod \to 0_{S} \in R$
17	14 16	syl	$⊢ φ \to 0_{S} \in R$
18	17	adantr	$⊢ (φ \land H = 0_{D}) \to 0_{S} \in R$
19		simpr	$⊢ (φ \land H = 0_{D}) \to H = 0_{D}$
20	3 1 15 5 6 11 14 8	ldual0vs	$⊢ φ \to 0_{S} \underset{˙}{\cdot} G = 0_{D}$
21	20	adantr	$⊢ (φ \land H = 0_{D}) \to 0_{S} \underset{˙}{\cdot} G = 0_{D}$
22	19 21	eqtr4d	$⊢ (φ \land H = 0_{D}) \to H = 0_{S} \underset{˙}{\cdot} G$
23		oveq1	$⊢ r = 0_{S} \to r \underset{˙}{\cdot} G = 0_{S} \underset{˙}{\cdot} G$
24	23	rspceeqv	$⊢ (0_{S} \in R \land H = 0_{S} \underset{˙}{\cdot} G) \to \exists r \in R H = r \underset{˙}{\cdot} G$
25	18 22 24	syl2anc	$⊢ (φ \land H = 0_{D}) \to \exists r \in R H = r \underset{˙}{\cdot} G$
26	25	ex	$⊢ φ \to (H = 0_{D} \to \exists r \in R H = r \underset{˙}{\cdot} G)$
27	26	adantld	$⊢ φ \to ((G \neq 0_{D} \land H = 0_{D}) \to \exists r \in R H = r \underset{˙}{\cdot} G)$
28	12 27	sylbid	$⊢ φ \to (K (G) \subset K (H) \to \exists r \in R H = r \underset{˙}{\cdot} G)$
29	28	imp	$⊢ (φ \land K (G) \subset K (H)) \to \exists r \in R H = r \underset{˙}{\cdot} G$
30	7	adantr	$⊢ (φ \land K (G) = K (H)) \to W \in LVec$
31	8	adantr	$⊢ (φ \land K (G) = K (H)) \to G \in F$
32	9	adantr	$⊢ (φ \land K (G) = K (H)) \to H \in F$
33		simpr	$⊢ (φ \land K (G) = K (H)) \to K (G) = K (H)$
34	1 2 3 4 5 6 30 31 32 33	eqlkr4	$⊢ (φ \land K (G) = K (H)) \to \exists r \in R H = r \underset{˙}{\cdot} G$
35	29 34	jaodan	$⊢ (φ \land (K (G) \subset K (H) \lor K (G) = K (H))) \to \exists r \in R H = r \underset{˙}{\cdot} G$
36	10 35	sylan2b	$⊢ (φ \land K (G) \subseteq K (H)) \to \exists r \in R H = r \underset{˙}{\cdot} G$
37	7	adantr	$⊢ (φ \land r \in R) \to W \in LVec$
38	8	adantr	$⊢ (φ \land r \in R) \to G \in F$
39		simpr	$⊢ (φ \land r \in R) \to r \in R$
40	1 2 3 4 5 6 37 38 39	lkrss	$⊢ (φ \land r \in R) \to K (G) \subseteq K (r \underset{˙}{\cdot} G)$
41	40	ex	$⊢ φ \to (r \in R \to K (G) \subseteq K (r \underset{˙}{\cdot} G))$
42		fveq2	$⊢ H = r \underset{˙}{\cdot} G \to K (H) = K (r \underset{˙}{\cdot} G)$
43	42	sseq2d	$⊢ H = r \underset{˙}{\cdot} G \to (K (G) \subseteq K (H) \leftrightarrow K (G) \subseteq K (r \underset{˙}{\cdot} G))$
44	43	biimprcd	$⊢ K (G) \subseteq K (r \underset{˙}{\cdot} G) \to (H = r \underset{˙}{\cdot} G \to K (G) \subseteq K (H))$
45	41 44	syl6	$⊢ φ \to (r \in R \to (H = r \underset{˙}{\cdot} G \to K (G) \subseteq K (H)))$
46	45	rexlimdv	$⊢ φ \to (\exists r \in R H = r \underset{˙}{\cdot} G \to K (G) \subseteq K (H))$
47	46	imp	$⊢ (φ \land \exists r \in R H = r \underset{˙}{\cdot} G) \to K (G) \subseteq K (H)$
48	36 47	impbida	$⊢ φ \to (K (G) \subseteq K (H) \leftrightarrow \exists r \in R H = r \underset{˙}{\cdot} G)$

Metamath Proof Explorer

Theorem lkrss2N

Proof