lkreqN

Description: Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lkreq.s	$⊢ S = Scalar (W)$
	lkreq.r	$⊢ R = {Base}_{S}$
	lkreq.o	$⊢ \underset{˙}{0} = 0_{S}$
	lkreq.f	$⊢ F = LFnl (W)$
	lkreq.k	$⊢ K = LKer (W)$
	lkreq.d	$⊢ D = LDual (W)$
	lkreq.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lkreq.w	$⊢ φ \to W \in LVec$
	lkreq.a	$⊢ φ \to A \in (R ∖ \{\underset{˙}{0}\})$
	lkreq.h	$⊢ φ \to H \in F$
	lkreq.g	$⊢ φ \to G = A \underset{˙}{\cdot} H$
Assertion	lkreqN	$⊢ φ \to K (G) = K (H)$

Proof

Step	Hyp	Ref	Expression
1		lkreq.s	$⊢ S = Scalar (W)$
2		lkreq.r	$⊢ R = {Base}_{S}$
3		lkreq.o	$⊢ \underset{˙}{0} = 0_{S}$
4		lkreq.f	$⊢ F = LFnl (W)$
5		lkreq.k	$⊢ K = LKer (W)$
6		lkreq.d	$⊢ D = LDual (W)$
7		lkreq.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
8		lkreq.w	$⊢ φ \to W \in LVec$
9		lkreq.a	$⊢ φ \to A \in (R ∖ \{\underset{˙}{0}\})$
10		lkreq.h	$⊢ φ \to H \in F$
11		lkreq.g	$⊢ φ \to G = A \underset{˙}{\cdot} H$
12	11	eqeq1d	$⊢ φ \to (G = 0_{D} \leftrightarrow A \underset{˙}{\cdot} H = 0_{D})$
13		eqid	$⊢ {Base}_{D} = {Base}_{D}$
14		eqid	$⊢ Scalar (D) = Scalar (D)$
15		eqid	$⊢ {Base}_{Scalar (D)} = {Base}_{Scalar (D)}$
16		eqid	$⊢ 0_{Scalar (D)} = 0_{Scalar (D)}$
17		eqid	$⊢ 0_{D} = 0_{D}$
18	6 8	lduallvec	$⊢ φ \to D \in LVec$
19	9	eldifad	$⊢ φ \to A \in R$
20	1 2 6 14 15 8	ldualsbase	$⊢ φ \to {Base}_{Scalar (D)} = R$
21	19 20	eleqtrrd	$⊢ φ \to A \in {Base}_{Scalar (D)}$
22	4 6 13 8 10	ldualelvbase	$⊢ φ \to H \in {Base}_{D}$
23	13 7 14 15 16 17 18 21 22	lvecvs0or	$⊢ φ \to (A \underset{˙}{\cdot} H = 0_{D} \leftrightarrow (A = 0_{Scalar (D)} \lor H = 0_{D}))$
24		lveclmod	$⊢ W \in LVec \to W \in LMod$
25	8 24	syl	$⊢ φ \to W \in LMod$
26	1 3 6 14 16 25	ldual0	$⊢ φ \to 0_{Scalar (D)} = \underset{˙}{0}$
27	26	eqeq2d	$⊢ φ \to (A = 0_{Scalar (D)} \leftrightarrow A = \underset{˙}{0})$
28		eldifsni	$⊢ A \in (R ∖ \{\underset{˙}{0}\}) \to A \neq \underset{˙}{0}$
29	9 28	syl	$⊢ φ \to A \neq \underset{˙}{0}$
30	29	a1d	$⊢ φ \to (H \neq 0_{D} \to A \neq \underset{˙}{0})$
31	30	necon4d	$⊢ φ \to (A = \underset{˙}{0} \to H = 0_{D})$
32	27 31	sylbid	$⊢ φ \to (A = 0_{Scalar (D)} \to H = 0_{D})$
33		idd	$⊢ φ \to (H = 0_{D} \to H = 0_{D})$
34	32 33	jaod	$⊢ φ \to ((A = 0_{Scalar (D)} \lor H = 0_{D}) \to H = 0_{D})$
35	23 34	sylbid	$⊢ φ \to (A \underset{˙}{\cdot} H = 0_{D} \to H = 0_{D})$
36	12 35	sylbid	$⊢ φ \to (G = 0_{D} \to H = 0_{D})$
37		nne	$⊢ \neg H \neq 0_{D} \leftrightarrow H = 0_{D}$
38	36 37	syl6ibr	$⊢ φ \to (G = 0_{D} \to \neg H \neq 0_{D})$
39	38	con3d	$⊢ φ \to (\neg \neg H \neq 0_{D} \to \neg G = 0_{D})$
40	39	orrd	$⊢ φ \to (\neg H \neq 0_{D} \lor \neg G = 0_{D})$
41		ianor	$⊢ \neg (H \neq 0_{D} \land G = 0_{D}) \leftrightarrow (\neg H \neq 0_{D} \lor \neg G = 0_{D})$
42	40 41	sylibr	$⊢ φ \to \neg (H \neq 0_{D} \land G = 0_{D})$
43	4 1 2 6 7 25 19 10	ldualvscl	$⊢ φ \to A \underset{˙}{\cdot} H \in F$
44	11 43	eqeltrd	$⊢ φ \to G \in F$
45	4 5 6 17 8 10 44	lkrpssN	$⊢ φ \to (K (H) \subset K (G) \leftrightarrow (H \neq 0_{D} \land G = 0_{D}))$
46		df-pss	$⊢ K (H) \subset K (G) \leftrightarrow (K (H) \subseteq K (G) \land K (H) \neq K (G))$
47	45 46	bitr3di	$⊢ φ \to ((H \neq 0_{D} \land G = 0_{D}) \leftrightarrow (K (H) \subseteq K (G) \land K (H) \neq K (G)))$
48	1 2 4 5 6 7 8 10 19	lkrss	$⊢ φ \to K (H) \subseteq K (A \underset{˙}{\cdot} H)$
49	11	fveq2d	$⊢ φ \to K (G) = K (A \underset{˙}{\cdot} H)$
50	48 49	sseqtrrd	$⊢ φ \to K (H) \subseteq K (G)$
51	50	biantrurd	$⊢ φ \to (K (H) \neq K (G) \leftrightarrow (K (H) \subseteq K (G) \land K (H) \neq K (G)))$
52	47 51	bitr4d	$⊢ φ \to ((H \neq 0_{D} \land G = 0_{D}) \leftrightarrow K (H) \neq K (G))$
53	52	necon2bbid	$⊢ φ \to (K (H) = K (G) \leftrightarrow \neg (H \neq 0_{D} \land G = 0_{D}))$
54	42 53	mpbird	$⊢ φ \to K (H) = K (G)$
55	54	eqcomd	$⊢ φ \to K (G) = K (H)$

Metamath Proof Explorer

Theorem lkreqN

Proof