dihord2cN

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014) (New usage is discouraged.)

	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})$
Assertion	dihord2cN	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ⟨f, O⟩ \in I (X \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		dihord2c.t	$⊢ T = LTrn (K) (W)$
12		dihord2c.r	$⊢ R = trL (K) (W)$
13		dihord2c.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
14		simp3	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
15		eqidd	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to O = O$
16		simp1	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (K \in HL \land W \in H)$
17		simp1l	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in HL$
18	17	hllatd	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in Lat$
19		simp2	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to X \in B$
20		simp1r	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in H$
21	1 6	lhpbase	$⊢ W \in H \to W \in B$
22	20 21	syl	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in B$
23	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
24	18 19 22 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to X \underset{˙}{\land} W \in B$
25	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
26	18 19 22 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
27	1 2 6 11 12 13 7	dibopelval3	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to (⟨f, O⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land O = O))$
28	16 24 26 27	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (⟨f, O⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land O = O))$
29	14 15 28	mpbir2and	$⊢ ((K \in HL \land W \in H) \land X \in B \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ⟨f, O⟩ \in I (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihord2cN

Proof