Theorem lkrlspeqN

Description: Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lkrlspeq.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrlspeq.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
	lkrlspeq.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lkrlspeq.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lkrlspeq.j	$$⊢N=\mathrm{LSpan}\left(D\right)$$
	lkrlspeq.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lkrlspeq.h	$$⊢\phi \to H\in F$$
	lkrlspeq.g	$$⊢\phi \to G\in \left(N\left(\left\{H\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	lkrlspeqN	$$⊢\phi \to L\left(G\right)=L\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		lkrlspeq.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		lkrlspeq.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
3		lkrlspeq.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		lkrlspeq.o	$$⊢\underset{\dot{}}{0}=0_D$$
5		lkrlspeq.j	$$⊢N=\mathrm{LSpan}\left(D\right)$$
6		lkrlspeq.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lkrlspeq.h	$$⊢\phi \to H\in F$$
8		lkrlspeq.g	$$⊢\phi \to G\in \left(N\left(\left\{H\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9	8	eldifad	$$⊢\phi \to G\in N\left(\left\{H\right\}\right)$$
10		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
11	6 10	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
12	3 11	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
13		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
14	1 3 13 6 7	ldualelvbase	$$⊢\phi \to H\in {\mathrm{Base}}_D$$
15		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
17		eqid	$$⊢{\cdot }_D={\cdot }_D$$
18	15 16 13 17 5	ellspsn	$$⊢\left(D\in \mathrm{LMod}\wedge H\in {\mathrm{Base}}_D\right)\to \left(G\in N\left(\left\{H\right\}\right)\leftrightarrow \exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}G=k{\cdot }_{D}H\right)$$
19	12 14 18	syl2anc	$$⊢\phi \to \left(G\in N\left(\left\{H\right\}\right)\leftrightarrow \exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}G=k{\cdot }_{D}H\right)$$
20	9 19	mpbid	$$⊢\phi \to \exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}G=k{\cdot }_{D}H$$
21		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
23	21 22 3 15 16 6	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
24	20 23	rexeqtrdv	$$⊢\phi \to \exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}G=k{\cdot }_{D}H$$
25		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
26	6	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to W\in \mathrm{LVec}$$
27		simp2	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
28		simp3	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to G=k{\cdot }_{D}H$$
29		eldifsni	$$⊢G\in \left(N\left(\left\{H\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to G\ne \underset{\dot{}}{0}$$
30	8 29	syl	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
31	30	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to G\ne \underset{\dot{}}{0}$$
32	28 31	eqnetrrd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to k{\cdot }_{D}H\ne \underset{\dot{}}{0}$$
33		eqid	$$⊢0_{\mathrm{Scalar}\left(D\right)}=0_{\mathrm{Scalar}\left(D\right)}$$
34	21 25 3 15 33 11	ldual0	$$⊢\phi \to 0_{\mathrm{Scalar}\left(D\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
35	34	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to 0_{\mathrm{Scalar}\left(D\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
36	35	eqeq2d	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to \left(k=0_{\mathrm{Scalar}\left(D\right)}\leftrightarrow k=0_{\mathrm{Scalar}\left(W\right)}\right)$$
37		orc	$$⊢k=0_{\mathrm{Scalar}\left(D\right)}\to \left(k=0_{\mathrm{Scalar}\left(D\right)}\vee H=\underset{\dot{}}{0}\right)$$
38	36 37	biimtrrdi	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to \left(k=0_{\mathrm{Scalar}\left(W\right)}\to \left(k=0_{\mathrm{Scalar}\left(D\right)}\vee H=\underset{\dot{}}{0}\right)\right)$$
39	3 6	lduallvec	$$⊢\phi \to D\in \mathrm{LVec}$$
40	39	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to D\in \mathrm{LVec}$$
41	23	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
42	27 41	eleqtrrd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
43	14	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to H\in {\mathrm{Base}}_D$$
44	13 17 15 16 33 4 40 42 43	lvecvs0or	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to \left(k{\cdot }_{D}H=\underset{\dot{}}{0}\leftrightarrow \left(k=0_{\mathrm{Scalar}\left(D\right)}\vee H=\underset{\dot{}}{0}\right)\right)$$
45	38 44	sylibrd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to \left(k=0_{\mathrm{Scalar}\left(W\right)}\to k{\cdot }_{D}H=\underset{\dot{}}{0}\right)$$
46	45	necon3d	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to \left(k{\cdot }_{D}H\ne \underset{\dot{}}{0}\to k\ne 0_{\mathrm{Scalar}\left(W\right)}\right)$$
47	32 46	mpd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to k\ne 0_{\mathrm{Scalar}\left(W\right)}$$
48		eldifsn	$$⊢k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\leftrightarrow \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge k\ne 0_{\mathrm{Scalar}\left(W\right)}\right)$$
49	27 47 48	sylanbrc	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
50	7	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to H\in F$$
51	21 22 25 1 2 3 17 26 49 50 28	lkreqN	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge G=k{\cdot }_{D}H\right)\to L\left(G\right)=L\left(H\right)$$
52	51	rexlimdv3a	$$⊢\phi \to \left(\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}G=k{\cdot }_{D}H\to L\left(G\right)=L\left(H\right)\right)$$
53	24 52	mpd	$$⊢\phi \to L\left(G\right)=L\left(H\right)$$