dihord10

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	dihord10	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (f) \underset{˙}{\leq} (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		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		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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (K \in HL \land W \in H)$
19		simp12	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
20		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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
21		simp31l	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s \in E$
22		simp31r	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g \in T$
23		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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩$
24	1 2 5 6 14 13 11 15 9 16 17	dihordlem7b	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (f = g \land O = s)$
25	24	simpld	$⊢ ((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 ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to f = g$
26	18 19 20 21 22 23 25	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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to f = g$
27	26	fveq2d	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (f) = R (g)$
28		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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$
29	27 28	eqbrtrd	$⊢ (((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 (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihord10

Proof