lclkrlem2y

Description: Lemma for lclkr . Restate the hypotheses for E and G to say their kernels are closed, in order to eliminate the generating vectors X and Y . (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2y.l	$⊢ L = LKer (U)$
	lclkrlem2y.h	$⊢ H = LHyp (K)$
	lclkrlem2y.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2y.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2y.f	$⊢ F = LFnl (U)$
	lclkrlem2y.d	$⊢ D = LDual (U)$
	lclkrlem2y.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2y.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2y.e	$⊢ φ \to E \in F$
	lclkrlem2y.g	$⊢ φ \to G \in F$
	lclkrlem2y.le	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E)$
	lclkrlem2y.lg	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
Assertion	lclkrlem2y	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2y.l	$⊢ L = LKer (U)$
2		lclkrlem2y.h	$⊢ H = LHyp (K)$
3		lclkrlem2y.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		lclkrlem2y.u	$⊢ U = DVecH (K) (W)$
5		lclkrlem2y.f	$⊢ F = LFnl (U)$
6		lclkrlem2y.d	$⊢ D = LDual (U)$
7		lclkrlem2y.p	$⊢ \underset{˙}{+} = +_{D}$
8		lclkrlem2y.k	$⊢ φ \to (K \in HL \land W \in H)$
9		lclkrlem2y.e	$⊢ φ \to E \in F$
10		lclkrlem2y.g	$⊢ φ \to G \in F$
11		lclkrlem2y.le	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E)$
12		lclkrlem2y.lg	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
13		eqid	$⊢ {Base}_{U} = {Base}_{U}$
14	2 3 4 13 5 1 8 10	lcfl8a	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G) \leftrightarrow \exists y \in {Base}_{U} L (G) = \underset{˙}{⊥} (\{y\}))$
15	12 14	mpbid	$⊢ φ \to \exists y \in {Base}_{U} L (G) = \underset{˙}{⊥} (\{y\})$
16	2 3 4 13 5 1 8 9	lcfl8a	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E) \leftrightarrow \exists x \in {Base}_{U} L (E) = \underset{˙}{⊥} (\{x\}))$
17	11 16	mpbid	$⊢ φ \to \exists x \in {Base}_{U} L (E) = \underset{˙}{⊥} (\{x\})$
18	8	3ad2ant1	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to (K \in HL \land W \in H)$
19		simp21	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to x \in {Base}_{U}$
20		simp23	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to y \in {Base}_{U}$
21	9	3ad2ant1	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to E \in F$
22	10	3ad2ant1	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to G \in F$
23		simp22	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to L (E) = \underset{˙}{⊥} (\{x\})$
24		simp3	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to L (G) = \underset{˙}{⊥} (\{y\})$
25	1 2 3 4 13 5 6 7 18 19 20 21 22 23 24	lclkrlem2x	$⊢ (φ \land (x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \land L (G) = \underset{˙}{⊥} (\{y\})) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$
26	25	3exp	$⊢ φ \to ((x \in {Base}_{U} \land L (E) = \underset{˙}{⊥} (\{x\}) \land y \in {Base}_{U}) \to (L (G) = \underset{˙}{⊥} (\{y\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)))$
27	26	3expd	$⊢ φ \to (x \in {Base}_{U} \to (L (E) = \underset{˙}{⊥} (\{x\}) \to (y \in {Base}_{U} \to (L (G) = \underset{˙}{⊥} (\{y\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)))))$
28	27	rexlimdv	$⊢ φ \to (\exists x \in {Base}_{U} L (E) = \underset{˙}{⊥} (\{x\}) \to (y \in {Base}_{U} \to (L (G) = \underset{˙}{⊥} (\{y\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G))))$
29	17 28	mpd	$⊢ φ \to (y \in {Base}_{U} \to (L (G) = \underset{˙}{⊥} (\{y\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)))$
30	29	rexlimdv	$⊢ φ \to (\exists y \in {Base}_{U} L (G) = \underset{˙}{⊥} (\{y\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G))$
31	15 30	mpd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E \underset{˙}{+} G))) = L (E \underset{˙}{+} G)$

Metamath Proof Explorer

Theorem lclkrlem2y

Proof