lkrpssN

Description: Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lkrpss.f	$⊢ F = LFnl (W)$
	lkrpss.k	$⊢ K = LKer (W)$
	lkrpss.d	$⊢ D = LDual (W)$
	lkrpss.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrpss.w	$⊢ φ \to W \in LVec$
	lkrpss.g	$⊢ φ \to G \in F$
	lkrpss.h	$⊢ φ \to H \in F$
Assertion	lkrpssN	$⊢ φ \to (K (G) \subset K (H) \leftrightarrow (G \neq \underset{˙}{0} \land H = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		lkrpss.f	$⊢ F = LFnl (W)$
2		lkrpss.k	$⊢ K = LKer (W)$
3		lkrpss.d	$⊢ D = LDual (W)$
4		lkrpss.o	$⊢ \underset{˙}{0} = 0_{D}$
5		lkrpss.w	$⊢ φ \to W \in LVec$
6		lkrpss.g	$⊢ φ \to G \in F$
7		lkrpss.h	$⊢ φ \to H \in F$
8		df-pss	$⊢ K (G) \subset K (H) \leftrightarrow (K (G) \subseteq K (H) \land K (G) \neq K (H))$
9		simpr	$⊢ (φ \land K (G) \subset K (H)) \to K (G) \subset K (H)$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11		lveclmod	$⊢ W \in LVec \to W \in LMod$
12	5 11	syl	$⊢ φ \to W \in LMod$
13	10 1 2 12 7	lkrssv	$⊢ φ \to K (H) \subseteq {Base}_{W}$
14	13	adantr	$⊢ (φ \land K (G) \subset K (H)) \to K (H) \subseteq {Base}_{W}$
15	9 14	psssstrd	$⊢ (φ \land K (G) \subset K (H)) \to K (G) \subset {Base}_{W}$
16	15	pssned	$⊢ (φ \land K (G) \subset K (H)) \to K (G) \neq {Base}_{W}$
17	8 16	sylan2br	$⊢ (φ \land (K (G) \subseteq K (H) \land K (G) \neq K (H))) \to K (G) \neq {Base}_{W}$
18		simplr	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to K (G) \subseteq K (H)$
19		eqid	$⊢ LSHyp (W) = LSHyp (W)$
20	5	ad2antrr	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to W \in LVec$
21		simpr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) \in LSHyp (W)) \to K (G) \in LSHyp (W)$
22		simplr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (H) \in LSHyp (W)$
23	13	ad3antrrr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (H) \subseteq {Base}_{W}$
24		simpr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (G) = {Base}_{W}$
25		simpllr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (G) \subseteq K (H)$
26	24 25	eqsstrrd	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to {Base}_{W} \subseteq K (H)$
27	23 26	eqssd	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (H) = {Base}_{W}$
28	10 19 1 2 5 7	lkrshp4	$⊢ φ \to (K (H) \neq {Base}_{W} \leftrightarrow K (H) \in LSHyp (W))$
29	28	ad3antrrr	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to (K (H) \neq {Base}_{W} \leftrightarrow K (H) \in LSHyp (W))$
30	29	necon1bbid	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to (\neg K (H) \in LSHyp (W) \leftrightarrow K (H) = {Base}_{W})$
31	27 30	mpbird	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to \neg K (H) \in LSHyp (W)$
32	22 31	pm2.21dd	$⊢ (((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \land K (G) = {Base}_{W}) \to K (G) \in LSHyp (W)$
33	10 19 1 2 5 6	lkrshpor	$⊢ φ \to (K (G) \in LSHyp (W) \lor K (G) = {Base}_{W})$
34	33	ad2antrr	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to (K (G) \in LSHyp (W) \lor K (G) = {Base}_{W})$
35	21 32 34	mpjaodan	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to K (G) \in LSHyp (W)$
36		simpr	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to K (H) \in LSHyp (W)$
37	19 20 35 36	lshpcmp	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to (K (G) \subseteq K (H) \leftrightarrow K (G) = K (H))$
38	18 37	mpbid	$⊢ ((φ \land K (G) \subseteq K (H)) \land K (H) \in LSHyp (W)) \to K (G) = K (H)$
39	38	ex	$⊢ (φ \land K (G) \subseteq K (H)) \to (K (H) \in LSHyp (W) \to K (G) = K (H))$
40	39	necon3ad	$⊢ (φ \land K (G) \subseteq K (H)) \to (K (G) \neq K (H) \to \neg K (H) \in LSHyp (W))$
41	40	impr	$⊢ (φ \land (K (G) \subseteq K (H) \land K (G) \neq K (H))) \to \neg K (H) \in LSHyp (W)$
42	28	necon1bbid	$⊢ φ \to (\neg K (H) \in LSHyp (W) \leftrightarrow K (H) = {Base}_{W})$
43	42	adantr	$⊢ (φ \land (K (G) \subseteq K (H) \land K (G) \neq K (H))) \to (\neg K (H) \in LSHyp (W) \leftrightarrow K (H) = {Base}_{W})$
44	41 43	mpbid	$⊢ (φ \land (K (G) \subseteq K (H) \land K (G) \neq K (H))) \to K (H) = {Base}_{W}$
45	17 44	jca	$⊢ (φ \land (K (G) \subseteq K (H) \land K (G) \neq K (H))) \to (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})$
46	10 1 2 12 6	lkrssv	$⊢ φ \to K (G) \subseteq {Base}_{W}$
47	46	adantr	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to K (G) \subseteq {Base}_{W}$
48		simprr	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to K (H) = {Base}_{W}$
49	48	eqcomd	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to {Base}_{W} = K (H)$
50	47 49	sseqtrd	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to K (G) \subseteq K (H)$
51		simprl	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to K (G) \neq {Base}_{W}$
52	51 49	neeqtrd	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to K (G) \neq K (H)$
53	50 52	jca	$⊢ (φ \land (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W})) \to (K (G) \subseteq K (H) \land K (G) \neq K (H))$
54	45 53	impbida	$⊢ φ \to ((K (G) \subseteq K (H) \land K (G) \neq K (H)) \leftrightarrow (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W}))$
55	8 54	bitrid	$⊢ φ \to (K (G) \subset K (H) \leftrightarrow (K (G) \neq {Base}_{W} \land K (H) = {Base}_{W}))$
56	10 1 2 3 4 12 6	lkr0f2	$⊢ φ \to (K (G) = {Base}_{W} \leftrightarrow G = \underset{˙}{0})$
57	56	necon3bid	$⊢ φ \to (K (G) \neq {Base}_{W} \leftrightarrow G \neq \underset{˙}{0})$
58	10 1 2 3 4 12 7	lkr0f2	$⊢ φ \to (K (H) = {Base}_{W} \leftrightarrow H = \underset{˙}{0})$
59	57 58	anbi12d	$⊢ φ \to ((K (G) \neq {Base}_{W} \land K (H) = {Base}_{W}) \leftrightarrow (G \neq \underset{˙}{0} \land H = \underset{˙}{0}))$
60	55 59	bitrd	$⊢ φ \to (K (G) \subset K (H) \leftrightarrow (G \neq \underset{˙}{0} \land H = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem lkrpssN

Proof