cdlemn2a

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

	Ref	Expression
Hypotheses	cdlemn2a.b	$⊢ B = {Base}_{K}$
	cdlemn2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn2a.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemn2a.a	$⊢ A = Atoms (K)$
	cdlemn2a.h	$⊢ H = LHyp (K)$
	cdlemn2a.t	$⊢ T = LTrn (K) (W)$
	cdlemn2a.r	$⊢ R = trL (K) (W)$
	cdlemn2a.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
	cdlemn2a.i	$⊢ I = DIsoB (K) (W)$
	cdlemn2a.u	$⊢ U = DVecH (K) (W)$
	cdlemn2a.n	$⊢ N = LSpan (U)$
	cdlemn2a.f	$⊢ F = (ι h \in T \| h (Q) = S)$
Assertion	cdlemn2a	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨F, O⟩\}) \subseteq I (X)$

Proof

Step	Hyp	Ref	Expression
1		cdlemn2a.b	$⊢ B = {Base}_{K}$
2		cdlemn2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn2a.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn2a.a	$⊢ A = Atoms (K)$
5		cdlemn2a.h	$⊢ H = LHyp (K)$
6		cdlemn2a.t	$⊢ T = LTrn (K) (W)$
7		cdlemn2a.r	$⊢ R = trL (K) (W)$
8		cdlemn2a.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
9		cdlemn2a.i	$⊢ I = DIsoB (K) (W)$
10		cdlemn2a.u	$⊢ U = DVecH (K) (W)$
11		cdlemn2a.n	$⊢ N = LSpan (U)$
12		cdlemn2a.f	$⊢ F = (ι h \in T \| h (Q) = S)$
13		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (K \in HL \land W \in H)$
14		simp21	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
15		simp22	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
16	2 4 5 6 12	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to F \in T$
17	13 14 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to F \in T$
18	1 5 6 7 8 10 9 11	dib1dim2	$⊢ ((K \in HL \land W \in H) \land F \in T) \to I (R (F)) = N (\{⟨F, O⟩\})$
19	13 17 18	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to I (R (F)) = N (\{⟨F, O⟩\})$
20	1 2 3 4 5 6 7 12	cdlemn2	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \underset{˙}{\leq} X$
21	1 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in B$
22	13 17 21	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \in B$
23	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
24	13 17 23	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \underset{˙}{\leq} W$
25		simp23	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (X \in B \land X \underset{˙}{\leq} W)$
26	1 2 5 9	dibord	$⊢ ((K \in HL \land W \in H) \land (R (F) \in B \land R (F) \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (I (R (F)) \subseteq I (X) \leftrightarrow R (F) \underset{˙}{\leq} X)$
27	13 22 24 25 26	syl121anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (I (R (F)) \subseteq I (X) \leftrightarrow R (F) \underset{˙}{\leq} X)$
28	20 27	mpbird	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to I (R (F)) \subseteq I (X)$
29	19 28	eqsstrrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to N (\{⟨F, O⟩\}) \subseteq I (X)$

Metamath Proof Explorer

Theorem cdlemn2a

Proof