lcfrlem16

	Ref	Expression
Hypotheses	lcf1o.h	$⊢ H = LHyp (K)$
	lcf1o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcf1o.u	$⊢ U = DVecH (K) (W)$
	lcf1o.v	$⊢ V = {Base}_{U}$
	lcf1o.a	$⊢ \underset{˙}{+} = +_{U}$
	lcf1o.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcf1o.s	$⊢ S = Scalar (U)$
	lcf1o.r	$⊢ R = {Base}_{S}$
	lcf1o.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcf1o.f	$⊢ F = LFnl (U)$
	lcf1o.l	$⊢ L = LKer (U)$
	lcf1o.d	$⊢ D = LDual (U)$
	lcf1o.q	$⊢ Q = 0_{D}$
	lcf1o.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcf1o.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))))$
	lcflo.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem16.p	$⊢ P = LSubSp (D)$
	lcfrlem16.g	$⊢ φ \to G \in P$
	lcfrlem16.gs	$⊢ φ \to G \subseteq C$
	lcfrlem16.m	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
	lcfrlem16.x	$⊢ φ \to X \in (E ∖ \{\underset{˙}{0}\})$
Assertion	lcfrlem16	$⊢ φ \to J (X) \in G$

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	$⊢ H = LHyp (K)$
2		lcf1o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcf1o.u	$⊢ U = DVecH (K) (W)$
4		lcf1o.v	$⊢ V = {Base}_{U}$
5		lcf1o.a	$⊢ \underset{˙}{+} = +_{U}$
6		lcf1o.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		lcf1o.s	$⊢ S = Scalar (U)$
8		lcf1o.r	$⊢ R = {Base}_{S}$
9		lcf1o.z	$⊢ \underset{˙}{0} = 0_{U}$
10		lcf1o.f	$⊢ F = LFnl (U)$
11		lcf1o.l	$⊢ L = LKer (U)$
12		lcf1o.d	$⊢ D = LDual (U)$
13		lcf1o.q	$⊢ Q = 0_{D}$
14		lcf1o.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
15		lcf1o.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))))$
16		lcflo.k	$⊢ φ \to (K \in HL \land W \in H)$
17		lcfrlem16.p	$⊢ P = LSubSp (D)$
18		lcfrlem16.g	$⊢ φ \to G \in P$
19		lcfrlem16.gs	$⊢ φ \to G \subseteq C$
20		lcfrlem16.m	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
21		lcfrlem16.x	$⊢ φ \to X \in (E ∖ \{\underset{˙}{0}\})$
22	21	eldifad	$⊢ φ \to X \in E$
23	22 20	eleqtrdi	$⊢ φ \to X \in ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
24		eliun	$⊢ X \in ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \leftrightarrow \exists g \in G X \in \underset{˙}{⊥} (L (g))$
25	23 24	sylib	$⊢ φ \to \exists g \in G X \in \underset{˙}{⊥} (L (g))$
26		eqid	$⊢ \cdot_{D} = \cdot_{D}$
27	1 3 16	dvhlvec	$⊢ φ \to U \in LVec$
28	27	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to U \in LVec$
29		eqid	$⊢ {Base}_{D} = {Base}_{D}$
30	29 17	lssel	$⊢ (G \in P \land g \in G) \to g \in {Base}_{D}$
31	18 30	sylan	$⊢ (φ \land g \in G) \to g \in {Base}_{D}$
32	1 3 16	dvhlmod	$⊢ φ \to U \in LMod$
33	10 12 29 32	ldualvbase	$⊢ φ \to {Base}_{D} = F$
34	33	adantr	$⊢ (φ \land g \in G) \to {Base}_{D} = F$
35	31 34	eleqtrd	$⊢ (φ \land g \in G) \to g \in F$
36	35	3adant3	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to g \in F$
37	16	adantr	$⊢ (φ \land g \in G) \to (K \in HL \land W \in H)$
38	32	adantr	$⊢ (φ \land g \in G) \to U \in LMod$
39	4 10 11 38 35	lkrssv	$⊢ (φ \land g \in G) \to L (g) \subseteq V$
40	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (g) \subseteq V) \to \underset{˙}{⊥} (L (g)) \subseteq V$
41	37 39 40	syl2anc	$⊢ (φ \land g \in G) \to \underset{˙}{⊥} (L (g)) \subseteq V$
42	41	ralrimiva	$⊢ φ \to \forall g \in G \underset{˙}{⊥} (L (g)) \subseteq V$
43		iunss	$⊢ ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \subseteq V \leftrightarrow \forall g \in G \underset{˙}{⊥} (L (g)) \subseteq V$
44	42 43	sylibr	$⊢ φ \to ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \subseteq V$
45	20 44	eqsstrid	$⊢ φ \to E \subseteq V$
46	45	ssdifd	$⊢ φ \to E ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
47	46 21	sseldd	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem10	$⊢ φ \to J (X) \in F$
49	48	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to J (X) \in F$
50		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
51	16	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to (K \in HL \land W \in H)$
52		simp3	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to X \in \underset{˙}{⊥} (L (g))$
53		eldifsni	$⊢ X \in (E ∖ \{\underset{˙}{0}\}) \to X \neq \underset{˙}{0}$
54	21 53	syl	$⊢ φ \to X \neq \underset{˙}{0}$
55	54	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to X \neq \underset{˙}{0}$
56		eldifsn	$⊢ X \in (\underset{˙}{⊥} (L (g)) ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in \underset{˙}{⊥} (L (g)) \land X \neq \underset{˙}{0})$
57	52 55 56	sylanbrc	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to X \in (\underset{˙}{⊥} (L (g)) ∖ \{\underset{˙}{0}\})$
58	1 2 3 4 9 10 11 51 36 57 50	dochsnkrlem2	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to \underset{˙}{⊥} (L (g)) \in LSAtoms (U)$
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem15	$⊢ φ \to X \in \underset{˙}{⊥} (L (J (X)))$
60		eldifsn	$⊢ X \in (\underset{˙}{⊥} (L (J (X))) ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in \underset{˙}{⊥} (L (J (X))) \land X \neq \underset{˙}{0})$
61	59 54 60	sylanbrc	$⊢ φ \to X \in (\underset{˙}{⊥} (L (J (X))) ∖ \{\underset{˙}{0}\})$
62	1 2 3 4 9 10 11 16 48 61 50	dochsnkrlem2	$⊢ φ \to \underset{˙}{⊥} (L (J (X))) \in LSAtoms (U)$
63	62	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to \underset{˙}{⊥} (L (J (X))) \in LSAtoms (U)$
64	59	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to X \in \underset{˙}{⊥} (L (J (X)))$
65	9 50 28 58 63 55 52 64	lsat2el	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to \underset{˙}{⊥} (L (g)) = \underset{˙}{⊥} (L (J (X)))$
66		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
67	19	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to G \subseteq C$
68		simp2	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to g \in G$
69	67 68	sseldd	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to g \in C$
70	1 66 2 3 10 11 14 51 36	lcfl5	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to (g \in C \leftrightarrow L (g) \in ran DIsoH (K) (W))$
71	69 70	mpbid	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to L (g) \in ran DIsoH (K) (W)$
72	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem13	$⊢ φ \to J (X) \in (C ∖ \{Q\})$
73	72	eldifad	$⊢ φ \to J (X) \in C$
74	1 66 2 3 10 11 14 16 48	lcfl5	$⊢ φ \to (J (X) \in C \leftrightarrow L (J (X)) \in ran DIsoH (K) (W))$
75	73 74	mpbid	$⊢ φ \to L (J (X)) \in ran DIsoH (K) (W)$
76	75	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to L (J (X)) \in ran DIsoH (K) (W)$
77	1 66 2 51 71 76	doch11	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to (\underset{˙}{⊥} (L (g)) = \underset{˙}{⊥} (L (J (X))) \leftrightarrow L (g) = L (J (X)))$
78	65 77	mpbid	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to L (g) = L (J (X))$
79	7 8 10 11 12 26 28 36 49 78	eqlkr4	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to \exists k \in R J (X) = k \cdot_{D} g$
80	32	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to U \in LMod$
81	80	adantr	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to U \in LMod$
82	18	3ad2ant1	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to G \in P$
83	82	adantr	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to G \in P$
84		simpr	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to k \in R$
85		simpl2	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to g \in G$
86	7 8 12 26 17 81 83 84 85	ldualssvscl	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to k \cdot_{D} g \in G$
87		eleq1	$⊢ J (X) = k \cdot_{D} g \to (J (X) \in G \leftrightarrow k \cdot_{D} g \in G)$
88	86 87	syl5ibrcom	$⊢ ((φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \land k \in R) \to (J (X) = k \cdot_{D} g \to J (X) \in G)$
89	88	rexlimdva	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to (\exists k \in R J (X) = k \cdot_{D} g \to J (X) \in G)$
90	79 89	mpd	$⊢ (φ \land g \in G \land X \in \underset{˙}{⊥} (L (g))) \to J (X) \in G$
91	90	rexlimdv3a	$⊢ φ \to (\exists g \in G X \in \underset{˙}{⊥} (L (g)) \to J (X) \in G)$
92	25 91	mpd	$⊢ φ \to J (X) \in G$

Metamath Proof Explorer

Theorem lcfrlem16

Proof