lcfrlem33

	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))$
	lcfrlem33.xi	$⊢ φ \to J (X) (I) = Q$
Assertion	lcfrlem33	$⊢ φ \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		lcfrlem33.xi	$⊢ φ \to J (X) (I) = Q$
27	26	oveq2d	$⊢ φ \to F (J (Y) (I)) \cdot_{S} J (X) (I) = F (J (Y) (I)) \cdot_{S} Q$
28	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
29	15	lmodring	$⊢ U \in LMod \to S \in Ring$
30	28 29	syl	$⊢ φ \to S \in Ring$
31	1 3 9	dvhlvec	$⊢ φ \to U \in LVec$
32	15	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
33	31 32	syl	$⊢ φ \to S \in DivRing$
34		eqid	$⊢ LFnl (U) = LFnl (U)$
35		eqid	$⊢ 0_{D} = 0_{D}$
36		eqid	$⊢ \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
37	1 2 3 4 5 14 15 17 6 34 20 21 35 36 18 9 11	lcfrlem10	$⊢ φ \to J (Y) \in LFnl (U)$
38	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$⊢ φ \to B \in A$
39	4 8 28 38	lsatssv	$⊢ φ \to B \subseteq V$
40	39 19	sseldd	$⊢ φ \to I \in V$
41	15 17 4 34	lflcl	$⊢ (U \in LMod \land J (Y) \in LFnl (U) \land I \in V) \to J (Y) (I) \in R$
42	28 37 40 41	syl3anc	$⊢ φ \to J (Y) (I) \in R$
43	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$
44	33 42 22 43	syl3anc	$⊢ φ \to F (J (Y) (I)) \in R$
45		eqid	$⊢ \cdot_{S} = \cdot_{S}$
46	17 45 16	ringrz	$⊢ (S \in Ring \land F (J (Y) (I)) \in R) \to F (J (Y) (I)) \cdot_{S} Q = Q$
47	30 44 46	syl2anc	$⊢ φ \to F (J (Y) (I)) \cdot_{S} Q = Q$
48	27 47	eqtrd	$⊢ φ \to F (J (Y) (I)) \cdot_{S} J (X) (I) = Q$
49	48	oveq1d	$⊢ φ \to (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y) = Q \cdot_{D} J (Y)$
50		eqid	$⊢ \cdot_{D} = \cdot_{D}$
51	34 15 16 21 50 35 28 37	ldual0vs	$⊢ φ \to Q \cdot_{D} J (Y) = 0_{D}$
52	49 51	eqtrd	$⊢ φ \to (F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y) = 0_{D}$
53	52	oveq2d	$⊢ φ \to J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = J (X) \underset{˙}{-} 0_{D}$
54	21 28	ldualgrp	$⊢ φ \to D \in Grp$
55		eqid	$⊢ {Base}_{D} = {Base}_{D}$
56	1 2 3 4 5 14 15 17 6 34 20 21 35 36 18 9 10	lcfrlem10	$⊢ φ \to J (X) \in LFnl (U)$
57	34 21 55 28 56	ldualelvbase	$⊢ φ \to J (X) \in {Base}_{D}$
58	55 35 24	grpsubid1	$⊢ (D \in Grp \land J (X) \in {Base}_{D}) \to J (X) \underset{˙}{-} 0_{D} = J (X)$
59	54 57 58	syl2anc	$⊢ φ \to J (X) \underset{˙}{-} 0_{D} = J (X)$
60	53 59	eqtrd	$⊢ φ \to J (X) \underset{˙}{-} ((F (J (Y) (I)) \cdot_{S} J (X) (I)) \cdot_{D} J (Y)) = J (X)$
61	25 60	eqtrid	$⊢ φ \to C = J (X)$
62	1 2 3 4 5 14 15 17 6 34 20 21 35 36 18 9 10	lcfrlem13	$⊢ φ \to J (X) \in (\{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} ∖ \{0_{D}\})$
63		eldifsni	$⊢ J (X) \in (\{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} ∖ \{0_{D}\}) \to J (X) \neq 0_{D}$
64	62 63	syl	$⊢ φ \to J (X) \neq 0_{D}$
65	61 64	eqnetrd	$⊢ φ \to C \neq 0_{D}$

Metamath Proof Explorer

Theorem lcfrlem33

Proof