lcfrlem31

	Ref	Expression
Hypotheses	lcfrlem17.h	$⊢ H = LHyp (K)$
	lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem17.u	$⊢ U = DVecH (K) (W)$
	lcfrlem17.v	$⊢ V = {Base}_{U}$
	lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfrlem17.n	$⊢ N = LSpan (U)$
	lcfrlem17.a	$⊢ A = LSAtoms (U)$
	lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
	lcfrlem24.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfrlem24.s	$⊢ S = Scalar (U)$
	lcfrlem24.q	$⊢ Q = 0_{S}$
	lcfrlem24.r	$⊢ R = {Base}_{S}$
	lcfrlem24.j	$⊢ J = (x \in (V ∖ \{\underset{˙}{0}\}) ⟼ (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
	lcfrlem24.ib	$⊢ φ \to I \in B$
	lcfrlem24.l	$⊢ L = LKer (U)$
	lcfrlem25.d	$⊢ D = LDual (U)$
	lcfrlem28.jn	$⊢ φ \to J (Y) (I) \neq Q$
	lcfrlem29.i	$⊢ F = {inv}_{r} (S)$
	lcfrlem30.m	$⊢ \underset{˙}{-} = -_{D}$
	lcfrlem30.c	$⊢ C = J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
	lcfrlem31.xi	$⊢ φ \to J (X) (I) \neq Q$
	lcfrlem31.cn	$⊢ φ \to C = 0_{D}$
Assertion	lcfrlem31	$⊢ φ \to N (\{X\}) = N (\{Y\})$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$⊢ H = LHyp (K)$
2		lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem17.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem17.v	$⊢ V = {Base}_{U}$
5		lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
6		lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
7		lcfrlem17.n	$⊢ N = LSpan (U)$
8		lcfrlem17.a	$⊢ A = LSAtoms (U)$
9		lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
11		lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
12		lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
13		lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
14		lcfrlem24.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
15		lcfrlem24.s	$⊢ S = Scalar (U)$
16		lcfrlem24.q	$⊢ Q = 0_{S}$
17		lcfrlem24.r	$⊢ R = {Base}_{S}$
18		lcfrlem24.j	$⊢ J = (x \in (V ∖ \{\underset{˙}{0}\}) ⟼ (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{x\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} x))))$
19		lcfrlem24.ib	$⊢ φ \to I \in B$
20		lcfrlem24.l	$⊢ L = LKer (U)$
21		lcfrlem25.d	$⊢ D = LDual (U)$
22		lcfrlem28.jn	$⊢ φ \to J (Y) (I) \neq Q$
23		lcfrlem29.i	$⊢ F = {inv}_{r} (S)$
24		lcfrlem30.m	$⊢ \underset{˙}{-} = -_{D}$
25		lcfrlem30.c	$⊢ C = J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
26		lcfrlem31.xi	$⊢ φ \to J (X) (I) \neq Q$
27		lcfrlem31.cn	$⊢ φ \to C = 0_{D}$
28	25 27	eqtr3id	$⊢ φ \to J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = 0_{D}$
29	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
30	21 29	lduallmod	$⊢ φ \to D \in LMod$
31		eqid	$⊢ LFnl (U) = LFnl (U)$
32		eqid	$⊢ {Base}_{D} = {Base}_{D}$
33		eqid	$⊢ 0_{D} = 0_{D}$
34		eqid	$⊢ \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
35	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10	lcfrlem10	$⊢ φ \to J (X) \in LFnl (U)$
36	31 21 32 29 35	ldualelvbase	$⊢ φ \to J (X) \in {Base}_{D}$
37		eqid	$⊢ \cdot_{D} = \cdot_{D}$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	lcfrlem29	$⊢ φ \to F (J (Y) (I)) \cdot_{S} J (X) (I) \in R$
39	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11	lcfrlem10	$⊢ φ \to J (Y) \in LFnl (U)$
40	31 15 17 21 37 29 38 39	ldualvscl	$⊢ φ \to (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y) \in LFnl (U)$
41	31 21 32 29 40	ldualelvbase	$⊢ φ \to (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y) \in {Base}_{D}$
42	32 33 24	lmodsubeq0	$⊢ (D \in LMod \land J (X) \in {Base}_{D} \land (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y) \in {Base}_{D}) \to (J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = 0_{D} \leftrightarrow J (X) = (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
43	30 36 41 42	syl3anc	$⊢ φ \to (J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = 0_{D} \leftrightarrow J (X) = (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
44	28 43	mpbid	$⊢ φ \to J (X) = (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)$
45	44	fveq2d	$⊢ φ \to L (J (X)) = L ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y))$
46	1 3 9	dvhlvec	$⊢ φ \to U \in LVec$
47	15	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
48	46 47	syl	$⊢ φ \to S \in DivRing$
49	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$⊢ φ \to B \in A$
50	4 8 29 49	lsatssv	$⊢ φ \to B \subseteq V$
51	50 19	sseldd	$⊢ φ \to I \in V$
52	15 17 4 31	lflcl	$⊢ (U \in LMod \land J (Y) \in LFnl (U) \land I \in V) \to J (Y) (I) \in R$
53	29 39 51 52	syl3anc	$⊢ φ \to J (Y) (I) \in R$
54	17 16 23	drnginvrn0	$⊢ (S \in DivRing \land J (Y) (I) \in R \land J (Y) (I) \neq Q) \to F (J (Y) (I)) \neq Q$
55	48 53 22 54	syl3anc	$⊢ φ \to F (J (Y) (I)) \neq Q$
56		eqid	$⊢ \cdot_{S} = \cdot_{S}$
57	17 16 23	drnginvrcl	$⊢ (S \in DivRing \land J (Y) (I) \in R \land J (Y) (I) \neq Q) \to F (J (Y) (I)) \in R$
58	48 53 22 57	syl3anc	$⊢ φ \to F (J (Y) (I)) \in R$
59	15 17 4 31	lflcl	$⊢ (U \in LMod \land J (X) \in LFnl (U) \land I \in V) \to J (X) (I) \in R$
60	29 35 51 59	syl3anc	$⊢ φ \to J (X) (I) \in R$
61	17 16 56 48 58 60	drngmulne0	$⊢ φ \to (F (J (Y) (I)) \cdot_{S} J (X) (I) \neq Q \leftrightarrow (F (J (Y) (I)) \neq Q \land J (X) (I) \neq Q))$
62	55 26 61	mpbir2and	$⊢ φ \to F (J (Y) (I)) \cdot_{S} J (X) (I) \neq Q$
63	15 17 16 31 20 21 37 46 39 38 62	ldualkrsc	$⊢ φ \to L ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = L (J (Y))$
64	45 63	eqtrd	$⊢ φ \to L (J (X)) = L (J (Y))$
65	64	fveq2d	$⊢ φ \to \underset{˙}{⊥} (L (J (X))) = \underset{˙}{⊥} (L (J (Y)))$
66	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10 7	lcfrlem14	$⊢ φ \to \underset{˙}{⊥} (L (J (X))) = N (\{X\})$
67	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11 7	lcfrlem14	$⊢ φ \to \underset{˙}{⊥} (L (J (Y))) = N (\{Y\})$
68	65 66 67	3eqtr3d	$⊢ φ \to N (\{X\}) = N (\{Y\})$

Metamath Proof Explorer

Theorem lcfrlem31

Proof