Theorem lkreqN

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

	Ref	Expression
Hypotheses	lkreq.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	lkreq.r	$$⊢R={\mathrm{Base}}_S$$
	lkreq.o	$$⊢\underset{\dot{}}{0}=0_S$$
	lkreq.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkreq.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
	lkreq.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lkreq.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lkreq.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lkreq.a	$$⊢\phi \to A\in \left(R\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lkreq.h	$$⊢\phi \to H\in F$$
	lkreq.g	$$⊢\phi \to G=A\underset{\dot{}}{·}H$$
Assertion	lkreqN	$$⊢\phi \to K\left(G\right)=K\left(H\right)$$

Proof

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