lvolcmp

Description: If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012)

	Ref	Expression
Hypotheses	lvolcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolcmp.v	$⊢ V = LVols (K)$
Assertion	lvolcmp	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		lvolcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolcmp.v	$⊢ V = LVols (K)$
3		simp2	$⊢ (K \in HL \land X \in V \land Y \in V) \to X \in V$
4		simp1	$⊢ (K \in HL \land X \in V \land Y \in V) \to K \in HL$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 2	lvolbase	$⊢ X \in V \to X \in {Base}_{K}$
7	6	3ad2ant2	$⊢ (K \in HL \land X \in V \land Y \in V) \to X \in {Base}_{K}$
8		eqid	$⊢ ⋖_{K} = ⋖_{K}$
9		eqid	$⊢ LPlanes (K) = LPlanes (K)$
10	5 8 9 2	islvol4	$⊢ (K \in HL \land X \in {Base}_{K}) \to (X \in V \leftrightarrow \exists z \in LPlanes (K) z ⋖_{K} X)$
11	4 7 10	syl2anc	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \in V \leftrightarrow \exists z \in LPlanes (K) z ⋖_{K} X)$
12	3 11	mpbid	$⊢ (K \in HL \land X \in V \land Y \in V) \to \exists z \in LPlanes (K) z ⋖_{K} X$
13		simpr3	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X \underset{˙}{\leq} Y$
14		hlpos	$⊢ K \in HL \to K \in Poset$
15	14	3ad2ant1	$⊢ (K \in HL \land X \in V \land Y \in V) \to K \in Poset$
16	15	adantr	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to K \in Poset$
17	7	adantr	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X \in {Base}_{K}$
18		simpl3	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in V$
19	5 2	lvolbase	$⊢ Y \in V \to Y \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in {Base}_{K}$
21		simpr1	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \in LPlanes (K)$
22	5 9	lplnbase	$⊢ z \in LPlanes (K) \to z \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \in {Base}_{K}$
24		simpr2	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z ⋖_{K} X$
25		simpl1	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to K \in HL$
26	5 1 8	cvrle	$⊢ ((K \in HL \land z \in {Base}_{K} \land X \in {Base}_{K}) \land z ⋖_{K} X) \to z \underset{˙}{\leq} X$
27	25 23 17 24 26	syl31anc	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \underset{˙}{\leq} X$
28	5 1	postr	$⊢ (K \in Poset \land (z \in {Base}_{K} \land X \in {Base}_{K} \land Y \in {Base}_{K})) \to ((z \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to z \underset{˙}{\leq} Y)$
29	16 23 17 20 28	syl13anc	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to ((z \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to z \underset{˙}{\leq} Y)$
30	27 13 29	mp2and	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \underset{˙}{\leq} Y$
31	1 8 9 2	lplncvrlvol2	$⊢ ((K \in HL \land z \in LPlanes (K) \land Y \in V) \land z \underset{˙}{\leq} Y) \to z ⋖_{K} Y$
32	25 21 18 30 31	syl31anc	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z ⋖_{K} Y$
33	5 1 8	cvrcmp	$⊢ (K \in Poset \land (X \in {Base}_{K} \land Y \in {Base}_{K} \land z \in {Base}_{K}) \land (z ⋖_{K} X \land z ⋖_{K} Y)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$
34	16 17 20 23 24 32 33	syl132anc	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$
35	13 34	mpbid	$⊢ ((K \in HL \land X \in V \land Y \in V) \land (z \in LPlanes (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X = Y$
36	35	3exp2	$⊢ (K \in HL \land X \in V \land Y \in V) \to (z \in LPlanes (K) \to (z ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y)))$
37	36	rexlimdv	$⊢ (K \in HL \land X \in V \land Y \in V) \to (\exists z \in LPlanes (K) z ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y))$
38	12 37	mpd	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \underset{˙}{\leq} Y \to X = Y)$
39	5 1	posref	$⊢ (K \in Poset \land X \in {Base}_{K}) \to X \underset{˙}{\leq} X$
40	15 7 39	syl2anc	$⊢ (K \in HL \land X \in V \land Y \in V) \to X \underset{˙}{\leq} X$
41		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
42	40 41	syl5ibcom	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X = Y \to X \underset{˙}{\leq} Y)$
43	38 42	impbid	$⊢ (K \in HL \land X \in V \land Y \in V) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem lvolcmp

Proof