trlord

Description: The ordering of two Hilbert lattice elements (under the fiducial hyperplane W ) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	trlord.b	$⊢ B = {Base}_{K}$
	trlord.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	trlord.a	$⊢ A = Atoms (K)$
	trlord.h	$⊢ H = LHyp (K)$
	trlord.t	$⊢ T = LTrn (K) (W)$
	trlord.r	$⊢ R = trL (K) (W)$
Assertion	trlord	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y))$

Proof

Step	Hyp	Ref	Expression
1		trlord.b	$⊢ B = {Base}_{K}$
2		trlord.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		trlord.a	$⊢ A = Atoms (K)$
4		trlord.h	$⊢ H = LHyp (K)$
5		trlord.t	$⊢ T = LTrn (K) (W)$
6		trlord.r	$⊢ R = trL (K) (W)$
7		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to K \in HL$
8	7	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to K \in Lat$
9		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to (K \in HL \land W \in H)$
10		simprlr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to f \in T$
11	1 4 5 6	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \in B$
12	9 10 11	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to R (f) \in B$
13		simpl2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to X \in B$
14		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to Y \in B$
15		simprr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to R (f) \underset{˙}{\leq} X$
16		simprll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to X \underset{˙}{\leq} Y$
17	1 2 8 12 13 14 15 16	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land ((X \underset{˙}{\leq} Y \land f \in T) \land R (f) \underset{˙}{\leq} X)) \to R (f) \underset{˙}{\leq} Y$
18	17	exp44	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \to (f \in T \to (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y)))$
19	18	ralrimdv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \to \forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y))$
20		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to K \in HL$
21	20	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to K \in Lat$
22		simp2r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to u \in A$
23	1 3	atbase	$⊢ u \in A \to u \in B$
24	22 23	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to u \in B$
25		simp12l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to X \in B$
26		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to W \in H$
27	1 4	lhpbase	$⊢ W \in H \to W \in B$
28	26 27	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to W \in B$
29		simp3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to u \underset{˙}{\leq} X$
30		simp12r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to X \underset{˙}{\leq} W$
31	1 2 21 24 25 28 29 30	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to u \underset{˙}{\leq} W$
32	31 29	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} X) \to (u \underset{˙}{\leq} W \land u \underset{˙}{\leq} X)$
33	32	3expia	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A)) \to (u \underset{˙}{\leq} X \to (u \underset{˙}{\leq} W \land u \underset{˙}{\leq} X))$
34		simp11	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
35		simp2r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to u \in A$
36		simp3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to u \underset{˙}{\leq} W$
37	2 3 4 5 6	cdlemf	$⊢ ((K \in HL \land W \in H) \land (u \in A \land u \underset{˙}{\leq} W)) \to \exists g \in T R (g) = u$
38	34 35 36 37	syl12anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to \exists g \in T R (g) = u$
39		simp2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to \forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y)$
40		fveq2	$⊢ f = g \to R (f) = R (g)$
41	40	breq1d	$⊢ f = g \to (R (f) \underset{˙}{\leq} X \leftrightarrow R (g) \underset{˙}{\leq} X)$
42	40	breq1d	$⊢ f = g \to (R (f) \underset{˙}{\leq} Y \leftrightarrow R (g) \underset{˙}{\leq} Y)$
43	41 42	imbi12d	$⊢ f = g \to ((R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \leftrightarrow (R (g) \underset{˙}{\leq} X \to R (g) \underset{˙}{\leq} Y))$
44	43	rspccv	$⊢ \forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \to (g \in T \to (R (g) \underset{˙}{\leq} X \to R (g) \underset{˙}{\leq} Y))$
45	39 44	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to (g \in T \to (R (g) \underset{˙}{\leq} X \to R (g) \underset{˙}{\leq} Y))$
46		breq1	$⊢ R (g) = u \to (R (g) \underset{˙}{\leq} X \leftrightarrow u \underset{˙}{\leq} X)$
47		breq1	$⊢ R (g) = u \to (R (g) \underset{˙}{\leq} Y \leftrightarrow u \underset{˙}{\leq} Y)$
48	46 47	imbi12d	$⊢ R (g) = u \to ((R (g) \underset{˙}{\leq} X \to R (g) \underset{˙}{\leq} Y) \leftrightarrow (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
49	48	biimpcd	$⊢ (R (g) \underset{˙}{\leq} X \to R (g) \underset{˙}{\leq} Y) \to (R (g) = u \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
50	45 49	syl6	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to (g \in T \to (R (g) = u \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y)))$
51	50	rexlimdv	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to (\exists g \in T R (g) = u \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
52	38 51	mpd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A) \land u \underset{˙}{\leq} W) \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y)$
53	52	3expia	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A)) \to (u \underset{˙}{\leq} W \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
54	53	impd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A)) \to ((u \underset{˙}{\leq} W \land u \underset{˙}{\leq} X) \to u \underset{˙}{\leq} Y)$
55	33 54	syld	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \land u \in A)) \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y)$
56	55	exp32	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \to (u \in A \to (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y)))$
57	56	ralrimdv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \to \forall u \in A (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
58		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in HL$
59		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in B$
60		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in B$
61	1 2 3	hlatle	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall u \in A (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
62	58 59 60 61	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall u \in A (u \underset{˙}{\leq} X \to u \underset{˙}{\leq} Y))$
63	57 62	sylibrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (\forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y)$
64	19 63	impbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\leq} Y \leftrightarrow \forall f \in T (R (f) \underset{˙}{\leq} X \to R (f) \underset{˙}{\leq} Y))$

Metamath Proof Explorer

Theorem trlord

Proof