lcfrlem42

Description: Lemma for lcfr . Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem38.h	$⊢ H = LHyp (K)$
	lcfrlem38.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem38.u	$⊢ U = DVecH (K) (W)$
	lcfrlem38.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem38.f	$⊢ F = LFnl (U)$
	lcfrlem38.l	$⊢ L = LKer (U)$
	lcfrlem38.d	$⊢ D = LDual (U)$
	lcfrlem38.q	$⊢ Q = LSubSp (D)$
	lcfrlem38.c	$⊢ C = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lcfrlem38.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
	lcfrlem38.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem38.g	$⊢ φ \to G \in Q$
	lcfrlem38.gs	$⊢ φ \to G \subseteq C$
	lcfrlem38.xe	$⊢ φ \to X \in E$
	lcfrlem38.ye	$⊢ φ \to Y \in E$
Assertion	lcfrlem42	$⊢ φ \to X \underset{˙}{+} Y \in E$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem38.h	$⊢ H = LHyp (K)$
2		lcfrlem38.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem38.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem38.p	$⊢ \underset{˙}{+} = +_{U}$
5		lcfrlem38.f	$⊢ F = LFnl (U)$
6		lcfrlem38.l	$⊢ L = LKer (U)$
7		lcfrlem38.d	$⊢ D = LDual (U)$
8		lcfrlem38.q	$⊢ Q = LSubSp (D)$
9		lcfrlem38.c	$⊢ C = \{f \in LFnl (U) \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
10		lcfrlem38.e	$⊢ E = ⋃_{g \in G} \underset{˙}{⊥} (L (g))$
11		lcfrlem38.k	$⊢ φ \to (K \in HL \land W \in H)$
12		lcfrlem38.g	$⊢ φ \to G \in Q$
13		lcfrlem38.gs	$⊢ φ \to G \subseteq C$
14		lcfrlem38.xe	$⊢ φ \to X \in E$
15		lcfrlem38.ye	$⊢ φ \to Y \in E$
16	1 3 11	dvhlmod	$⊢ φ \to U \in LMod$
17		eqid	$⊢ {Base}_{U} = {Base}_{U}$
18	1 2 3 17 6 7 8 10 11 12 14	lcfrlem4	$⊢ φ \to X \in {Base}_{U}$
19	1 2 3 17 6 7 8 10 11 12 15	lcfrlem4	$⊢ φ \to Y \in {Base}_{U}$
20	17 4	lmodcom	$⊢ (U \in LMod \land X \in {Base}_{U} \land Y \in {Base}_{U}) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
21	16 18 19 20	syl3anc	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
22	21	adantr	$⊢ (φ \land X = 0_{U}) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
23	11	adantr	$⊢ (φ \land X = 0_{U}) \to (K \in HL \land W \in H)$
24	12	adantr	$⊢ (φ \land X = 0_{U}) \to G \in Q$
25	15	adantr	$⊢ (φ \land X = 0_{U}) \to Y \in E$
26		eqid	$⊢ 0_{U} = 0_{U}$
27		simpr	$⊢ (φ \land X = 0_{U}) \to X = 0_{U}$
28	1 2 3 4 6 7 8 23 24 10 25 26 27	lcfrlem7	$⊢ (φ \land X = 0_{U}) \to Y \underset{˙}{+} X \in E$
29	22 28	eqeltrd	$⊢ (φ \land X = 0_{U}) \to X \underset{˙}{+} Y \in E$
30	11	adantr	$⊢ (φ \land Y = 0_{U}) \to (K \in HL \land W \in H)$
31	12	adantr	$⊢ (φ \land Y = 0_{U}) \to G \in Q$
32	14	adantr	$⊢ (φ \land Y = 0_{U}) \to X \in E$
33		simpr	$⊢ (φ \land Y = 0_{U}) \to Y = 0_{U}$
34	1 2 3 4 6 7 8 30 31 10 32 26 33	lcfrlem7	$⊢ (φ \land Y = 0_{U}) \to X \underset{˙}{+} Y \in E$
35	11	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to (K \in HL \land W \in H)$
36	12	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to G \in Q$
37	13	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to G \subseteq C$
38	14	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \in E$
39	15	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \in E$
40		simprl	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \neq 0_{U}$
41		simprr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \neq 0_{U}$
42	1 2 3 4 5 6 7 8 9 10 35 36 37 38 39 26 40 41	lcfrlem41	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \underset{˙}{+} Y \in E$
43	29 34 42	pm2.61da2ne	$⊢ φ \to X \underset{˙}{+} Y \in E$

Metamath Proof Explorer

Theorem lcfrlem42

Proof