lcfrlem4

	Ref	Expression
Hypotheses	lcfrlem4.h	$⊢ H = LHyp (K)$
	lcfrlem4.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem4.u	$⊢ U = DVecH (K) (W)$
	lcfrlem4.v	$⊢ V = {Base}_{U}$
	lcfrlem4.l	$⊢ L = LKer (U)$
	lcfrlem4.d	$⊢ D = LDual (U)$
	lcfrlem4.q	$⊢ Q = LSubSp (D)$
	lcfrlem4.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
	lcfrlem4.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem4.g	$⊢ φ \to G \in Q$
	lcfrlem4.x	$⊢ φ \to X \in E$
Assertion	lcfrlem4	$⊢ φ \to X \in V$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem4.h	$⊢ H = LHyp (K)$
2		lcfrlem4.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem4.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem4.v	$⊢ V = {Base}_{U}$
5		lcfrlem4.l	$⊢ L = LKer (U)$
6		lcfrlem4.d	$⊢ D = LDual (U)$
7		lcfrlem4.q	$⊢ Q = LSubSp (D)$
8		lcfrlem4.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
9		lcfrlem4.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem4.g	$⊢ φ \to G \in Q$
11		lcfrlem4.x	$⊢ φ \to X \in E$
12	9	adantr	$⊢ (φ \land g \in G) \to (K \in HL \land W \in H)$
13		eqid	$⊢ LFnl (U) = LFnl (U)$
14	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
15	14	adantr	$⊢ (φ \land g \in G) \to U \in LMod$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17	16 7	lssel	$⊢ (G \in Q \land g \in G) \to g \in {Base}_{D}$
18	10 17	sylan	$⊢ (φ \land g \in G) \to g \in {Base}_{D}$
19	13 6 16 14	ldualvbase	$⊢ φ \to {Base}_{D} = LFnl (U)$
20	19	adantr	$⊢ (φ \land g \in G) \to {Base}_{D} = LFnl (U)$
21	18 20	eleqtrd	$⊢ (φ \land g \in G) \to g \in LFnl (U)$
22	4 13 5 15 21	lkrssv	$⊢ (φ \land g \in G) \to L (g) \subseteq V$
23	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land L (g) \subseteq V) \to \underset{˙}{⊥} (L (g)) \subseteq V$
24	12 22 23	syl2anc	$⊢ (φ \land g \in G) \to \underset{˙}{⊥} (L (g)) \subseteq V$
25	24	ralrimiva	$⊢ φ \to \forall g \in G \underset{˙}{⊥} (L (g)) \subseteq V$
26		iunss	$⊢ ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \subseteq V \leftrightarrow \forall g \in G \underset{˙}{⊥} (L (g)) \subseteq V$
27	25 26	sylibr	$⊢ φ \to ⋃_{g \in G} \underset{˙}{⊥} (L (g)) \subseteq V$
28	11 8	eleqtrdi	$⊢ φ \to X \in ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
29	27 28	sseldd	$⊢ φ \to X \in V$

Metamath Proof Explorer

Theorem lcfrlem4

Proof