lcfrlem34

	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))$
Assertion	lcfrlem34	$⊢ φ \to C \neq 0_{D}$

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	9	adantr	$⊢ (φ \land J (X) (I) = Q) \to (K \in HL \land W \in H)$
27	10	adantr	$⊢ (φ \land J (X) (I) = Q) \to X \in (V ∖ \{\underset{˙}{0}\})$
28	11	adantr	$⊢ (φ \land J (X) (I) = Q) \to Y \in (V ∖ \{\underset{˙}{0}\})$
29	12	adantr	$⊢ (φ \land J (X) (I) = Q) \to N (\{X\}) \neq N (\{Y\})$
30	19	adantr	$⊢ (φ \land J (X) (I) = Q) \to I \in B$
31	22	adantr	$⊢ (φ \land J (X) (I) = Q) \to J (Y) (I) \neq Q$
32		simpr	$⊢ (φ \land J (X) (I) = Q) \to J (X) (I) = Q$
33	1 2 3 4 5 6 7 8 26 27 28 29 13 14 15 16 17 18 30 20 21 31 23 24 25 32	lcfrlem33	$⊢ (φ \land J (X) (I) = Q) \to C \neq 0_{D}$
34	9	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to (K \in HL \land W \in H)$
35	10	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to X \in (V ∖ \{\underset{˙}{0}\})$
36	11	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to Y \in (V ∖ \{\underset{˙}{0}\})$
37	12	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to N (\{X\}) \neq N (\{Y\})$
38	19	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to I \in B$
39	22	adantr	$⊢ (φ \land J (X) (I) \neq Q) \to J (Y) (I) \neq Q$
40		simpr	$⊢ (φ \land J (X) (I) \neq Q) \to J (X) (I) \neq Q$
41	1 2 3 4 5 6 7 8 34 35 36 37 13 14 15 16 17 18 38 20 21 39 23 24 25 40	lcfrlem32	$⊢ (φ \land J (X) (I) \neq Q) \to C \neq 0_{D}$
42	33 41	pm2.61dane	$⊢ φ \to C \neq 0_{D}$

Metamath Proof Explorer

Theorem lcfrlem34

Proof