cdlemn11c

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

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

Proof

Step	Hyp	Ref	Expression
1		cdlemn11a.b	$⊢ B = {Base}_{K}$
2		cdlemn11a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn11a.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn11a.a	$⊢ A = Atoms (K)$
5		cdlemn11a.h	$⊢ H = LHyp (K)$
6		cdlemn11a.p	$⊢ P = oc (K) (W)$
7		cdlemn11a.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
8		cdlemn11a.t	$⊢ T = LTrn (K) (W)$
9		cdlemn11a.r	$⊢ R = trL (K) (W)$
10		cdlemn11a.e	$⊢ E = TEndo (K) (W)$
11		cdlemn11a.i	$⊢ I = DIsoB (K) (W)$
12		cdlemn11a.J	$⊢ J = DIsoC (K) (W)$
13		cdlemn11a.u	$⊢ U = DVecH (K) (W)$
14		cdlemn11a.d	$⊢ \underset{˙}{+} = +_{U}$
15		cdlemn11a.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
16		cdlemn11a.f	$⊢ F = (ι h \in T \| h (P) = Q)$
17		cdlemn11a.g	$⊢ G = (ι h \in T \| h (P) = N)$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	cdlemn11b	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to ⟨G, {I ↾}_{T}⟩ \in (J (Q) \underset{˙}{\oplus} I (X))$
19		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (K \in HL \land W \in H)$
20	5 13 19	dvhlmod	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to U \in LMod$
21		eqid	$⊢ LSubSp (U) = LSubSp (U)$
22	21	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
23	20 22	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to LSubSp (U) \subseteq SubGrp (U)$
24		simp21	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
25	2 4 5 13 12 21	diclss	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to J (Q) \in LSubSp (U)$
26	19 24 25	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to J (Q) \in LSubSp (U)$
27	23 26	sseldd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to J (Q) \in SubGrp (U)$
28		simp23l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to X \in B$
29		simp23r	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to X \underset{˙}{\leq} W$
30	1 2 5 13 11 21	diblss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \in LSubSp (U)$
31	19 28 29 30	syl12anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to I (X) \in LSubSp (U)$
32	23 31	sseldd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to I (X) \in SubGrp (U)$
33	14 15	lsmelval	$⊢ (J (Q) \in SubGrp (U) \land I (X) \in SubGrp (U)) \to (⟨G, {I ↾}_{T}⟩ \in (J (Q) \underset{˙}{\oplus} I (X)) \leftrightarrow \exists y \in J (Q) \exists z \in I (X) ⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z)$
34	27 32 33	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (⟨G, {I ↾}_{T}⟩ \in (J (Q) \underset{˙}{\oplus} I (X)) \leftrightarrow \exists y \in J (Q) \exists z \in I (X) ⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z)$
35	18 34	mpbid	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to \exists y \in J (Q) \exists z \in I (X) ⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z$

Metamath Proof Explorer

Theorem cdlemn11c

Proof