lclkrlem2c

	Ref	Expression
Hypotheses	lclkrlem2a.h	$⊢ H = LHyp (K)$
	lclkrlem2a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2a.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2a.v	$⊢ V = {Base}_{U}$
	lclkrlem2a.z	$⊢ \underset{˙}{0} = 0_{U}$
	lclkrlem2a.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2a.n	$⊢ N = LSpan (U)$
	lclkrlem2a.a	$⊢ A = LSAtoms (U)$
	lclkrlem2a.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2a.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.e	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\})$
	lclkrlem2b.da	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
	lclkrlem2c.j	$⊢ J = LSHyp (U)$
Assertion	lclkrlem2c	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) \underset{˙}{\oplus} N (\{B\}) \in J$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2a.h	$⊢ H = LHyp (K)$
2		lclkrlem2a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem2a.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem2a.v	$⊢ V = {Base}_{U}$
5		lclkrlem2a.z	$⊢ \underset{˙}{0} = 0_{U}$
6		lclkrlem2a.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
7		lclkrlem2a.n	$⊢ N = LSpan (U)$
8		lclkrlem2a.a	$⊢ A = LSAtoms (U)$
9		lclkrlem2a.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lclkrlem2a.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
11		lclkrlem2a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
12		lclkrlem2a.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
13		lclkrlem2a.e	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\})$
14		lclkrlem2b.da	$⊢ φ \to (\neg X \in \underset{˙}{⊥} (\{B\}) \lor \neg Y \in \underset{˙}{⊥} (\{B\}))$
15		lclkrlem2c.j	$⊢ J = LSHyp (U)$
16		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
17		eqid	$⊢ joinH (K) (W) = joinH (K) (W)$
18	11	eldifad	$⊢ φ \to X \in V$
19	1 3 4 7 16	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran DIsoH (K) (W)$
20	9 18 19	syl2anc	$⊢ φ \to N (\{X\}) \in ran DIsoH (K) (W)$
21	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
22	4 7 5 8 21 12	lsatlspsn	$⊢ φ \to N (\{Y\}) \in A$
23	1 16 3 6 8 9 20 22	dihsmatrn	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in ran DIsoH (K) (W)$
24	10	eldifad	$⊢ φ \to B \in V$
25	24	snssd	$⊢ φ \to \{B\} \subseteq V$
26	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{B\} \subseteq V) \to \underset{˙}{⊥} (\{B\}) \in ran DIsoH (K) (W)$
27	9 25 26	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{B\}) \in ran DIsoH (K) (W)$
28	1 16 3 4 2 17 9 23 27	dochdmm1	$⊢ φ \to \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\})) = \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (\{B\}))$
29	12	eldifad	$⊢ φ \to Y \in V$
30	4 7 6 21 18 29	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$
31		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
32	31	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
33	30 32	eqtr3di	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\} \cup \{Y\})$
34	33	fveq2d	$⊢ φ \to \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) = \underset{˙}{⊥} (N (\{X\} \cup \{Y\}))$
35	18	snssd	$⊢ φ \to \{X\} \subseteq V$
36	29	snssd	$⊢ φ \to \{Y\} \subseteq V$
37	35 36	unssd	$⊢ φ \to \{X\} \cup \{Y\} \subseteq V$
38	1 3 2 4 7 9 37	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X\} \cup \{Y\})) = \underset{˙}{⊥} (\{X\} \cup \{Y\})$
39	1 3 4 2	dochdmj1	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
40	9 35 36 39	syl3anc	$⊢ φ \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
41	34 38 40	3eqtrd	$⊢ φ \to \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
42	1 3 2 4 7 9 24	dochocsn	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{B\})) = N (\{B\})$
43	41 42	oveq12d	$⊢ φ \to \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (\{B\})) = (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) joinH (K) (W) N (\{B\})$
44	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V) \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
45	9 35 44	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W)$
46	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{Y\} \subseteq V) \to \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
47	9 36 46	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
48	1 16	dihmeetcl	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{⊥} (\{X\}) \in ran DIsoH (K) (W) \land \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W))) \to \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
49	9 45 47 48	syl12anc	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\}) \in ran DIsoH (K) (W)$
50	1 3 4 6 7 16 17 9 49 24	dihjat1	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) joinH (K) (W) N (\{B\}) = (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) \underset{˙}{\oplus} N (\{B\})$
51	28 43 50	3eqtrrd	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) \underset{˙}{\oplus} N (\{B\}) = \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}))$
52	1 2 3 4 5 6 7 8 9 10 11 12 13 14	lclkrlem2b	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$
53	1 3 2 8 15 9 52	dochsatshp	$⊢ φ \to \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\})) \in J$
54	51 53	eqeltrd	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})) \underset{˙}{\oplus} N (\{B\}) \in J$

Metamath Proof Explorer

Theorem lclkrlem2c

Proof