lplncmp

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

	Ref	Expression
Hypotheses	lplncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplncmp.p	$⊢ P = LPlanes (K)$
Assertion	lplncmp	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		lplncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplncmp.p	$⊢ P = LPlanes (K)$
3		simp2	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \in P$
4		simp1	$⊢ (K \in HL \land X \in P \land Y \in P) \to K \in HL$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 2	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
7	6	3ad2ant2	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \in {Base}_{K}$
8		eqid	$⊢ ⋖_{K} = ⋖_{K}$
9		eqid	$⊢ LLines (K) = LLines (K)$
10	5 8 9 2	islpln4	$⊢ (K \in HL \land X \in {Base}_{K}) \to (X \in P \leftrightarrow \exists z \in LLines (K) z ⋖_{K} X)$
11	4 7 10	syl2anc	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \in P \leftrightarrow \exists z \in LLines (K) z ⋖_{K} X)$
12	3 11	mpbid	$⊢ (K \in HL \land X \in P \land Y \in P) \to \exists z \in LLines (K) z ⋖_{K} X$
13		simpr3	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \to K \in Poset$
16	15	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to K \in Poset$
17	7	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X \in {Base}_{K}$
18		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in P$
19	5 2	lplnbase	$⊢ Y \in P \to Y \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in {Base}_{K}$
21		simpr1	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \in LLines (K)$
22	5 9	llnbase	$⊢ z \in LLines (K) \to z \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \in {Base}_{K}$
24		simpr2	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z ⋖_{K} X$
25		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to z \underset{˙}{\leq} Y$
31	1 8 9 2	llncvrlpln2	$⊢ ((K \in HL \land z \in LLines (K) \land Y \in P) \land z \underset{˙}{\leq} Y) \to z ⋖_{K} Y$
32	25 21 18 30 31	syl31anc	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \land (z \in LLines (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 P \land Y \in P) \land (z \in LLines (K) \land z ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X = Y$
36	35	3exp2	$⊢ (K \in HL \land X \in P \land Y \in P) \to (z \in LLines (K) \to (z ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y)))$
37	36	rexlimdv	$⊢ (K \in HL \land X \in P \land Y \in P) \to (\exists z \in LLines (K) z ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y))$
38	12 37	mpd	$⊢ (K \in HL \land X \in P \land Y \in P) \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 P \land Y \in P) \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 P \land Y \in P) \to (X = Y \to X \underset{˙}{\leq} Y)$
43	38 42	impbid	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem lplncmp

Proof