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 = LFnl (W)$
	lkrlspeq.l	$⊢ L = LKer (W)$
	lkrlspeq.d	$⊢ D = LDual (W)$
	lkrlspeq.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrlspeq.j	$⊢ N = LSpan (D)$
	lkrlspeq.w	$⊢ φ \to W \in LVec$
	lkrlspeq.h	$⊢ φ \to H \in F$
	lkrlspeq.g	$⊢ φ \to G \in (N (\{H\}) ∖ \{\underset{˙}{0}\})$
Assertion	lkrlspeqN	$⊢ φ \to L (G) = L (H)$

Proof

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

Metamath Proof Explorer

Theorem lkrlspeqN

Proof