cdlemn5pre

Description: Part of proof of Lemma N of Crawley p. 121 line 32. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn5.b	$⊢ B = {Base}_{K}$
	cdlemn5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn5.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemn5.a	$⊢ A = Atoms (K)$
	cdlemn5.h	$⊢ H = LHyp (K)$
	cdlemn5.u	$⊢ U = DVecH (K) (W)$
	cdlemn5.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	cdlemn5.i	$⊢ I = DIsoB (K) (W)$
	cdlemn5.J	$⊢ J = DIsoC (K) (W)$
	cdlemn5.p	$⊢ P = oc (K) (W)$
	cdlemn5.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	cdlemn5.t	$⊢ T = LTrn (K) (W)$
	cdlemn5.e	$⊢ E = TEndo (K) (W)$
	cdlemn5.n	$⊢ N = LSpan (U)$
	cdlemn5.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn5.g	$⊢ G = (ι h \in T \| h (P) = R)$
	cdlemn5.m	$⊢ M = (ι h \in T \| h (Q) = R)$
Assertion	cdlemn5pre	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (R) \subseteq J (Q) \underset{˙}{\oplus} I (X)$

Proof

Step	Hyp	Ref	Expression
1		cdlemn5.b	$⊢ B = {Base}_{K}$
2		cdlemn5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn5.a	$⊢ A = Atoms (K)$
5		cdlemn5.h	$⊢ H = LHyp (K)$
6		cdlemn5.u	$⊢ U = DVecH (K) (W)$
7		cdlemn5.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
8		cdlemn5.i	$⊢ I = DIsoB (K) (W)$
9		cdlemn5.J	$⊢ J = DIsoC (K) (W)$
10		cdlemn5.p	$⊢ P = oc (K) (W)$
11		cdlemn5.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
12		cdlemn5.t	$⊢ T = LTrn (K) (W)$
13		cdlemn5.e	$⊢ E = TEndo (K) (W)$
14		cdlemn5.n	$⊢ N = LSpan (U)$
15		cdlemn5.f	$⊢ F = (ι h \in T \| h (P) = Q)$
16		cdlemn5.g	$⊢ G = (ι h \in T \| h (P) = R)$
17		cdlemn5.m	$⊢ M = (ι h \in T \| h (Q) = R)$
18		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (K \in HL \land W \in H)$
19		simp22	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
20	2 4 5 10 12 9 6 14 16	diclspsn	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J (R) = N (\{⟨G, {I ↾}_{T}⟩\})$
21	18 19 20	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (R) = N (\{⟨G, {I ↾}_{T}⟩\})$
22		simp21	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
23	1 2 4 10 5 12 11 6 15 16 17 14 7	cdlemn4a	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨M, O⟩\})$
24	18 22 19 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨M, O⟩\})$
25	2 4 5 10 12 9 6 14 15	diclspsn	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to J (Q) = N (\{⟨F, {I ↾}_{T}⟩\})$
26	18 22 25	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (Q) = N (\{⟨F, {I ↾}_{T}⟩\})$
27	26	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (Q) \underset{˙}{\oplus} N (\{⟨M, O⟩\}) = N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨M, O⟩\})$
28	24 27	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq J (Q) \underset{˙}{\oplus} N (\{⟨M, O⟩\})$
29	5 6 18	dvhlmod	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to U \in LMod$
30		eqid	$⊢ LSubSp (U) = LSubSp (U)$
31	30	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
32	29 31	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to LSubSp (U) \subseteq SubGrp (U)$
33	2 4 5 6 9 30	diclss	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to J (Q) \in LSubSp (U)$
34	18 22 33	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (Q) \in LSubSp (U)$
35	32 34	sseldd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (Q) \in SubGrp (U)$
36		simp23	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (X \in B \land X \underset{˙}{\leq} W)$
37	1 2 5 6 8 30	diblss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \in LSubSp (U)$
38	18 36 37	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to I (X) \in LSubSp (U)$
39	32 38	sseldd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to I (X) \in SubGrp (U)$
40		eqid	$⊢ trL (K) (W) = trL (K) (W)$
41	1 2 3 4 5 12 40 11 8 6 14 17	cdlemn2a	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨M, O⟩\}) \subseteq I (X)$
42	7	lsmless2	$⊢ (J (Q) \in SubGrp (U) \land I (X) \in SubGrp (U) \land N (\{⟨M, O⟩\}) \subseteq I (X)) \to J (Q) \underset{˙}{\oplus} N (\{⟨M, O⟩\}) \subseteq J (Q) \underset{˙}{\oplus} I (X)$
43	35 39 41 42	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (Q) \underset{˙}{\oplus} N (\{⟨M, O⟩\}) \subseteq J (Q) \underset{˙}{\oplus} I (X)$
44	28 43	sstrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq J (Q) \underset{˙}{\oplus} I (X)$
45	21 44	eqsstrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to J (R) \subseteq J (Q) \underset{˙}{\oplus} I (X)$

Metamath Proof Explorer

Theorem cdlemn5pre

Proof