lclkrlem2h

Description: Lemma for lclkr . Eliminate the ( L( E .+ G ) ) e. J hypothesis. (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2f.h	$⊢ H = LHyp (K)$
	lclkrlem2f.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2f.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2f.v	$⊢ V = {Base}_{U}$
	lclkrlem2f.s	$⊢ S = Scalar (U)$
	lclkrlem2f.q	$⊢ Q = 0_{S}$
	lclkrlem2f.z	$⊢ \underset{˙}{0} = 0_{U}$
	lclkrlem2f.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2f.n	$⊢ N = LSpan (U)$
	lclkrlem2f.f	$⊢ F = LFnl (U)$
	lclkrlem2f.j	$⊢ J = LSHyp (U)$
	lclkrlem2f.l	$⊢ L = LKer (U)$
	lclkrlem2f.d	$⊢ D = LDual (U)$
	lclkrlem2f.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2f.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2f.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2f.e	$⊢ φ \to E \in F$
	lclkrlem2f.g	$⊢ φ \to G \in F$
	lclkrlem2f.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
	lclkrlem2f.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
	lclkrlem2f.kb	$⊢ φ \to (E \underset{˙}{+} G) (B) = Q$
	lclkrlem2f.nx	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
	lclkrlem2h.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2h.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2h.ne	$⊢ φ \to L (E) \neq L (G)$
Assertion	lclkrlem2h	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2f.h	$⊢ H = LHyp (K)$
2		lclkrlem2f.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem2f.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem2f.v	$⊢ V = {Base}_{U}$
5		lclkrlem2f.s	$⊢ S = Scalar (U)$
6		lclkrlem2f.q	$⊢ Q = 0_{S}$
7		lclkrlem2f.z	$⊢ \underset{˙}{0} = 0_{U}$
8		lclkrlem2f.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		lclkrlem2f.n	$⊢ N = LSpan (U)$
10		lclkrlem2f.f	$⊢ F = LFnl (U)$
11		lclkrlem2f.j	$⊢ J = LSHyp (U)$
12		lclkrlem2f.l	$⊢ L = LKer (U)$
13		lclkrlem2f.d	$⊢ D = LDual (U)$
14		lclkrlem2f.p	$⊢ \underset{˙}{+} = +_{D}$
15		lclkrlem2f.k	$⊢ φ \to (K \in HL \land W \in H)$
16		lclkrlem2f.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
17		lclkrlem2f.e	$⊢ φ \to E \in F$
18		lclkrlem2f.g	$⊢ φ \to G \in F$
19		lclkrlem2f.le	$⊢ φ \to L (E) = \underset{˙}{⊥} (\{X\})$
20		lclkrlem2f.lg	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
21		lclkrlem2f.kb	$⊢ φ \to (E \underset{˙}{+} G) (B) = Q$
22		lclkrlem2f.nx	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
23		lclkrlem2h.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
24		lclkrlem2h.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
25		lclkrlem2h.ne	$⊢ φ \to L (E) \neq L (G)$
26	15	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to (K \in HL \land W \in H)$
27	16	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to B \in (V ∖ \{\underset{˙}{0}\})$
28	17	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to E \in F$
29	18	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to G \in F$
30	19	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to L (E) = \underset{˙}{⊥} (\{X\})$
31	20	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to L (G) = \underset{˙}{⊥} (\{Y\})$
32	21	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to (E \underset{˙}{+} G) (B) = Q$
33	22	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
34	23	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to X \in (V ∖ \{\underset{˙}{0}\})$
35	24	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to Y \in (V ∖ \{\underset{˙}{0}\})$
36	25	adantr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to L (E) \neq L (G)$
37		simpr	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to L (E \underset{˙}{+} G) \in J$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 27 28 29 30 31 32 33 34 35 36 37	lclkrlem2g	$⊢ (φ \land L (E \underset{˙}{+} G) \in J) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
39	1 3 2 4 15	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
40	39	adantr	$⊢ (φ \land \neg L (E \underset{˙}{+} G) \in J) \to \underset{˙}{⊥} (\underset{˙}{⊥} (V)) = V$
41	1 3 15	dvhlvec	$⊢ φ \to U \in LVec$
42	1 3 15	dvhlmod	$⊢ φ \to U \in LMod$
43	10 13 14 42 17 18	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
44	4 11 10 12 41 43	lkrshpor	$⊢ φ \to (L (E \underset{˙}{+} G) \in J \lor L (E \underset{˙}{+} G) = V)$
45	44	orcanai	$⊢ (φ \land \neg L (E \underset{˙}{+} G) \in J) \to L (E \underset{˙}{+} G) = V$
46	45	fveq2d	$⊢ (φ \land \neg L (E \underset{˙}{+} G) \in J) \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) = \underset{˙}{⊥} (V)$
47	46	fveq2d	$⊢ (φ \land \neg L (E \underset{˙}{+} G) \in J) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (V))$
48	40 47 45	3eqtr4d	$⊢ (φ \land \neg L (E \underset{˙}{+} G) \in J) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
49	38 48	pm2.61dan	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Metamath Proof Explorer

Theorem lclkrlem2h

Proof