dihord11c

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)$
	dihord2c.t	$⊢ T = LTrn (K) (W)$
	dihord2c.r	$⊢ R = trL (K) (W)$
	dihord2c.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dihord2.p	$⊢ P = oc (K) (W)$
	dihord2.e	$⊢ E = TEndo (K) (W)$
	dihord2.d	$⊢ \underset{˙}{+} = +_{U}$
	dihord2.g	$⊢ G = (ι h \in T \| h (P) = N)$
Assertion	dihord11c	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z$

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		dihord2c.t	$⊢ T = LTrn (K) (W)$
12		dihord2c.r	$⊢ R = trL (K) (W)$
13		dihord2c.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
14		dihord2.p	$⊢ P = oc (K) (W)$
15		dihord2.e	$⊢ E = TEndo (K) (W)$
16		dihord2.d	$⊢ \underset{˙}{+} = +_{U}$
17		dihord2.g	$⊢ G = (ι h \in T \| h (P) = N)$
18		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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((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))$
19		simp2	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (X \in B \land Y \in B)$
20		simp31	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)$
21		simp32	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to f \in T$
22		simp33	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	dihord11b	$⊢ ((((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 Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ⟨f, O⟩ \in (J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W))$
24	18 19 20 21 22 23	syl32anc	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ⟨f, O⟩ \in (J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W))$
25		simp11	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (K \in HL \land W \in H)$
26	6 9 25	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to U \in LMod$
27		eqid	$⊢ LSubSp (U) = LSubSp (U)$
28	27	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
29	26 28	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to LSubSp (U) \subseteq SubGrp (U)$
30		simp13	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
31	2 5 6 9 8 27	diclss	$⊢ ((K \in HL \land W \in H) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \to J (N) \in LSubSp (U)$
32	25 30 31	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to J (N) \in LSubSp (U)$
33	29 32	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to J (N) \in SubGrp (U)$
34		simp11l	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in HL$
35	34	hllatd	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in Lat$
36		simp2r	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to Y \in B$
37		simp11r	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in H$
38	1 6	lhpbase	$⊢ W \in H \to W \in B$
39	37 38	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in B$
40	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
41	35 36 39 40	syl3anc	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to Y \underset{˙}{\land} W \in B$
42	1 2 4	latmle2	$⊢ (K \in Lat \land Y \in B \land W \in B) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
43	35 36 39 42	syl3anc	$⊢ (((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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
44	1 2 6 9 7 27	diblss	$⊢ ((K \in HL \land W \in H) \land (Y \underset{˙}{\land} W \in B \land (Y \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} W) \in LSubSp (U)$
45	25 41 43 44	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to I (Y \underset{˙}{\land} W) \in LSubSp (U)$
46	29 45	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to I (Y \underset{˙}{\land} W) \in SubGrp (U)$
47	16 10	lsmelval	$⊢ (J (N) \in SubGrp (U) \land I (Y \underset{˙}{\land} W) \in SubGrp (U)) \to (⟨f, O⟩ \in (J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \leftrightarrow \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z)$
48	33 46 47	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (⟨f, O⟩ \in (J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \leftrightarrow \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z)$
49	24 48	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 Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z$

Metamath Proof Explorer

Theorem dihord11c

Proof