lclkrlem2b

	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\}))$
Assertion	lclkrlem2b	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$

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	9	adantr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to (K \in HL \land W \in H)$
16	10	adantr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to B \in (V ∖ \{\underset{˙}{0}\})$
17	11	adantr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
18	12	adantr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
19	13	adantr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to \underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\})$
20		simpr	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to \neg X \in \underset{˙}{⊥} (\{B\})$
21	1 2 3 4 5 6 7 8 15 16 17 18 19 20	lclkrlem2a	$⊢ (φ \land \neg X \in \underset{˙}{⊥} (\{B\})) \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$
22	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
23		lmodabl	$⊢ U \in LMod \to U \in Abel$
24	22 23	syl	$⊢ φ \to U \in Abel$
25		eqid	$⊢ LSubSp (U) = LSubSp (U)$
26	25	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
27	22 26	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
28	11	eldifad	$⊢ φ \to X \in V$
29	4 25 7	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
30	22 28 29	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
31	27 30	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (U)$
32	12	eldifad	$⊢ φ \to Y \in V$
33	4 25 7	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
34	22 32 33	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
35	27 34	sseldd	$⊢ φ \to N (\{Y\}) \in SubGrp (U)$
36	6	lsmcom	$⊢ (U \in Abel \land N (\{X\}) \in SubGrp (U) \land N (\{Y\}) \in SubGrp (U)) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{Y\}) \underset{˙}{\oplus} N (\{X\})$
37	24 31 35 36	syl3anc	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{Y\}) \underset{˙}{\oplus} N (\{X\})$
38	37	ineq1d	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) = (N (\{Y\}) \underset{˙}{\oplus} N (\{X\})) \cap \underset{˙}{⊥} (\{B\})$
39	38	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) = (N (\{Y\}) \underset{˙}{\oplus} N (\{X\})) \cap \underset{˙}{⊥} (\{B\})$
40	9	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to (K \in HL \land W \in H)$
41	10	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to B \in (V ∖ \{\underset{˙}{0}\})$
42	12	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
43	11	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
44	13	necomd	$⊢ φ \to \underset{˙}{⊥} (\{Y\}) \neq \underset{˙}{⊥} (\{X\})$
45	44	adantr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to \underset{˙}{⊥} (\{Y\}) \neq \underset{˙}{⊥} (\{X\})$
46		simpr	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to \neg Y \in \underset{˙}{⊥} (\{B\})$
47	1 2 3 4 5 6 7 8 40 41 42 43 45 46	lclkrlem2a	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to (N (\{Y\}) \underset{˙}{\oplus} N (\{X\})) \cap \underset{˙}{⊥} (\{B\}) \in A$
48	39 47	eqeltrd	$⊢ (φ \land \neg Y \in \underset{˙}{⊥} (\{B\})) \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$
49	21 48 14	mpjaodan	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$

Metamath Proof Explorer

Theorem lclkrlem2b

Proof