dihord2b

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dihjust.b	$⊢ B = {Base}_{K}$
	dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihjust.a	$⊢ A = Atoms (K)$
	dihjust.h	$⊢ H = LHyp (K)$
	dihjust.i	$⊢ I = DIsoB (K) (W)$
	dihjust.J	$⊢ J = DIsoC (K) (W)$
	dihjust.u	$⊢ U = DVecH (K) (W)$
	dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	dihord2b	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	$⊢ B = {Base}_{K}$
2		dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihjust.a	$⊢ A = Atoms (K)$
6		dihjust.h	$⊢ H = LHyp (K)$
7		dihjust.i	$⊢ I = DIsoB (K) (W)$
8		dihjust.J	$⊢ J = DIsoC (K) (W)$
9		dihjust.u	$⊢ U = DVecH (K) (W)$
10		dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
11		simp11	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (K \in HL \land W \in H)$
12	6 9 11	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to U \in LMod$
13		eqid	$⊢ LSubSp (U) = LSubSp (U)$
14	13	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
15	12 14	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to LSubSp (U) \subseteq SubGrp (U)$
16		simp12	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
17	2 5 6 9 8 13	diclss	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to J (Q) \in LSubSp (U)$
18	11 16 17	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to J (Q) \in LSubSp (U)$
19	15 18	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to J (Q) \in SubGrp (U)$
20		simp11l	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to K \in HL$
21	20	hllatd	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to K \in Lat$
22		simp2l	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to X \in B$
23		simp11r	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to W \in H$
24	1 6	lhpbase	$⊢ W \in H \to W \in B$
25	23 24	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to W \in B$
26	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
27	21 22 25 26	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to X \underset{˙}{\land} W \in B$
28	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
29	21 22 25 28	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
30	1 2 6 9 7 13	diblss	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) \in LSubSp (U)$
31	11 27 29 30	syl12anc	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to I (X \underset{˙}{\land} W) \in LSubSp (U)$
32	15 31	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to I (X \underset{˙}{\land} W) \in SubGrp (U)$
33	10	lsmub2	$⊢ (J (Q) \in SubGrp (U) \land I (X \underset{˙}{\land} W) \in SubGrp (U)) \to I (X \underset{˙}{\land} W) \subseteq J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$
34	19 32 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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to I (X \underset{˙}{\land} W) \subseteq J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$
35		simp3	$⊢ (((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)$
36	34 35	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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihord2b

Proof