cdlemn11pre

Description: Part of proof of Lemma N of Crawley p. 121 line 37. TODO: combine cdlemn11a , cdlemn11b , cdlemn11c , cdlemn11pre into one? (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	cdlemn11pre	$⊢ ((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 N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$

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	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$
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		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)$
21	2 4 5 6 8 10 12 16	dicelval3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (y \in J (Q) \leftrightarrow \exists s \in E y = ⟨s (F), s⟩)$
22	19 20 21	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 (y \in J (Q) \leftrightarrow \exists s \in E y = ⟨s (F), s⟩)$
23		simp23	$⊢ ((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 \land X \underset{˙}{\leq} W)$
24	1 2 5 8 9 7 11	dibelval3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (z \in I (X) \leftrightarrow \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X))$
25	19 23 24	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 (z \in I (X) \leftrightarrow \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X))$
26	22 25	anbi12d	$⊢ ((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 ((y \in J (Q) \land z \in I (X)) \leftrightarrow (\exists s \in E y = ⟨s (F), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)))$
27		reeanv	$⊢ \exists s \in E \exists g \in T (y = ⟨s (F), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \leftrightarrow (\exists s \in E y = ⟨s (F), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X))$
28		simpl1	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (K \in HL \land W \in H)$
29		simpl21	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
30		simpl22	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
31		simpl23	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (X \in B \land X \underset{˙}{\leq} W)$
32		simpr1r	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g \in T$
33		simpr1l	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s \in E$
34		simpr3	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩$
35	1 2 4 5 6 7 8 10 13 14 16 17	cdlemn9	$⊢ ((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 (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g (Q) = N$
36	28 29 30 33 32 34 35	syl123anc	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g (Q) = N$
37		simpr2	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (g) \underset{˙}{\leq} X$
38	1 2 3 4 5 8 9	cdlemn10	$⊢ ((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 (g \in T \land g (Q) = N \land R (g) \underset{˙}{\leq} X)) \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
39	28 29 30 31 32 36 37 38	syl133anc	$⊢ (((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)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} X \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
40	39	3exp2	$⊢ ((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 ((s \in E \land g \in T) \to (R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))))$
41		oveq12	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to y \underset{˙}{+} z = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩$
42	41	eqeq2d	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \leftrightarrow ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)$
43	42	imbi1d	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to ((⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \leftrightarrow (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
44	43	imbi2d	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to ((R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))) \leftrightarrow (R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))))$
45	44	biimprd	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to ((R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))) \to (R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))))$
46	45	com23	$⊢ (y = ⟨s (F), s⟩ \land z = ⟨g, O⟩) \to (R (g) \underset{˙}{\leq} X \to ((R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))))$
47	46	impr	$⊢ (y = ⟨s (F), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \to ((R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
48	47	com12	$⊢ (R (g) \underset{˙}{\leq} X \to (⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))) \to ((y = ⟨s (F), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
49	40 48	syl6	$⊢ ((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 ((s \in E \land g \in T) \to ((y = ⟨s (F), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))))$
50	49	rexlimdvv	$⊢ ((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 s \in E \exists g \in T (y = ⟨s (F), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
51	27 50	syl5bir	$⊢ ((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 s \in E y = ⟨s (F), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} X)) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
52	26 51	sylbid	$⊢ ((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 ((y \in J (Q) \land z \in I (X)) \to (⟨G, {I ↾}_{T}⟩ = y \underset{˙}{+} z \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)))$
53	52	rexlimdvv	$⊢ ((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 \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} X))$
54	18 53	mpd	$⊢ ((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 N \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$

Metamath Proof Explorer

Theorem cdlemn11pre

Proof