ps-2

Description: Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in MaedaMaeda p. 68 and part of Theorem 16.4 in MaedaMaeda p. 69. (Contributed by NM, 1-Dec-2011)

	Ref	Expression
Hypotheses	ps1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ps1.j	$⊢ \underset{˙}{\lor} = join (K)$
	ps1.a	$⊢ A = Atoms (K)$
Assertion	ps-2	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$

Proof

Step	Hyp	Ref	Expression
1		ps1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ps1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		ps1.a	$⊢ A = Atoms (K)$
4		simpl21	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S = P) \to P \in A$
5		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to K \in HL$
6		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \in A$
7		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to R \in A$
8	1 2 3	hlatlej1	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
9	5 6 7 8	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
10	9	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S = P) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
11		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to T \in A$
12	1 2 3	hlatlej1	$⊢ (K \in HL \land P \in A \land T \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} T)$
13	5 6 11 12	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} T)$
14		oveq1	$⊢ S = P \to S \underset{˙}{\lor} T = P \underset{˙}{\lor} T$
15	14	breq2d	$⊢ S = P \to (P \underset{˙}{\leq} (S \underset{˙}{\lor} T) \leftrightarrow P \underset{˙}{\leq} (P \underset{˙}{\lor} T))$
16	13 15	syl5ibrcom	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (S = P \to P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
17	16	imp	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S = P) \to P \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
18		breq1	$⊢ u = P \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
19		breq1	$⊢ u = P \to (u \underset{˙}{\leq} (S \underset{˙}{\lor} T) \leftrightarrow P \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
20	18 19	anbi12d	$⊢ u = P \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow (P \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
21	20	rspcev	$⊢ (P \in A \land (P \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land P \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
22	4 10 17 21	syl12anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S = P) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
23	22	a1d	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S = P) \to (((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
24		hlop	$⊢ K \in HL \to K \in OP$
25	24	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to K \in OP$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27		eqid	$⊢ 0. (K) = 0. (K)$
28	26 27	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
29	25 28	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to 0. (K) \in {Base}_{K}$
30	26 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
31	6 30	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \in {Base}_{K}$
32		eqid	$⊢ ⋖_{K} = ⋖_{K}$
33	27 32 3	atcvr0	$⊢ (K \in HL \land P \in A) \to 0. (K) ⋖_{K} P$
34	5 6 33	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to 0. (K) ⋖_{K} P$
35		eqid	$⊢ <_{K} = <_{K}$
36	26 35 32	cvrlt	$⊢ ((K \in HL \land 0. (K) \in {Base}_{K} \land P \in {Base}_{K}) \land 0. (K) ⋖_{K} P) \to 0. (K) <_{K} P$
37	5 29 31 34 36	syl31anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to 0. (K) <_{K} P$
38		hlpos	$⊢ K \in HL \to K \in Poset$
39	38	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to K \in Poset$
40		hllat	$⊢ K \in HL \to K \in Lat$
41	40	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to K \in Lat$
42	26 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
43	7 42	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to R \in {Base}_{K}$
44	26 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \underset{˙}{\lor} R \in {Base}_{K}$
45	41 31 43 44	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\lor} R \in {Base}_{K}$
46	26 1 35	pltletr	$⊢ (K \in Poset \land (0. (K) \in {Base}_{K} \land P \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K})) \to ((0. (K) <_{K} P \land P \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to 0. (K) <_{K} (P \underset{˙}{\lor} R))$
47	39 29 31 45 46	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to ((0. (K) <_{K} P \land P \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to 0. (K) <_{K} (P \underset{˙}{\lor} R))$
48	37 9 47	mp2and	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to 0. (K) <_{K} (P \underset{˙}{\lor} R)$
49	35	pltne	$⊢ (K \in HL \land 0. (K) \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K}) \to (0. (K) <_{K} (P \underset{˙}{\lor} R) \to 0. (K) \neq P \underset{˙}{\lor} R)$
50	5 29 45 49	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (0. (K) <_{K} (P \underset{˙}{\lor} R) \to 0. (K) \neq P \underset{˙}{\lor} R)$
51	48 50	mpd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to 0. (K) \neq P \underset{˙}{\lor} R$
52	51	necomd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\lor} R \neq 0. (K)$
53	52	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \underset{˙}{\lor} R \neq 0. (K)$
54		hlatl	$⊢ K \in HL \to K \in AtLat$
55	54	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to K \in AtLat$
56		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to S \in A$
57	1 3	atncmp	$⊢ (K \in AtLat \land S \in A \land P \in A) \to (\neg S \underset{˙}{\leq} P \leftrightarrow S \neq P)$
58	55 56 6 57	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (\neg S \underset{˙}{\leq} P \leftrightarrow S \neq P)$
59		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to Q \in A$
60	26 1 2 3	hlexch1	$⊢ (K \in HL \land (S \in A \land Q \in A \land P \in {Base}_{K}) \land \neg S \underset{˙}{\leq} P) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S))$
61	60	3expia	$⊢ (K \in HL \land (S \in A \land Q \in A \land P \in {Base}_{K})) \to (\neg S \underset{˙}{\leq} P \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S)))$
62	5 56 59 31 61	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (\neg S \underset{˙}{\leq} P \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S)))$
63	58 62	sylbird	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (S \neq P \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S)))$
64	63	imp32	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
65	26 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
66	59 65	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to Q \in {Base}_{K}$
67	26 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
68	56 67	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to S \in {Base}_{K}$
69	26 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land S \in {Base}_{K}) \to P \underset{˙}{\lor} S \in {Base}_{K}$
70	41 31 68 69	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to P \underset{˙}{\lor} S \in {Base}_{K}$
71	26 1 2	latjlej1	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land R \in {Base}_{K})) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
72	41 66 70 43 71	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
73	72	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
74	64 73	mpd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R)$
75	74	adantrrr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R)$
76	26 3	atbase	$⊢ T \in A \to T \in {Base}_{K}$
77	11 76	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to T \in {Base}_{K}$
78	26 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
79	41 66 43 78	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
80	26 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} R \in {Base}_{K}$
81	41 70 43 80	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} R \in {Base}_{K}$
82	26 1	lattr	$⊢ (K \in Lat \land (T \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\lor} R \in {Base}_{K})) \to ((T \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R)) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
83	41 77 79 81 82	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to ((T \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R)) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
84	83	expdimp	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
85	84	adantrl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
86	85	adantrl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R))$
87	75 86	mpd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R)$
88	2 3	hlatj32	$⊢ (K \in HL \land (P \in A \land S \in A \land R \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} R = (P \underset{˙}{\lor} R) \underset{˙}{\lor} S$
89	5 6 56 7 88	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} R = (P \underset{˙}{\lor} R) \underset{˙}{\lor} S$
90	89	breq2d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R) \leftrightarrow T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
91	90	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} S) \underset{˙}{\lor} R) \leftrightarrow T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
92	87 91	mpbid	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
93	53 92	jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (P \underset{˙}{\lor} R \neq 0. (K) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
94	93	adantrrl	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land (S \neq P \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))))) \to (P \underset{˙}{\lor} R \neq 0. (K) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
95	94	ex	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to ((S \neq P \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (P \underset{˙}{\lor} R \neq 0. (K) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)))$
96	26 1 2 27 3	cvrat4	$⊢ (K \in HL \land (P \underset{˙}{\lor} R \in {Base}_{K} \land T \in A \land S \in A)) \to ((P \underset{˙}{\lor} R \neq 0. (K) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)))$
97	5 45 11 56 96	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to ((P \underset{˙}{\lor} R \neq 0. (K) \land T \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)))$
98	95 97	syld	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to ((S \neq P \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)))$
99	98	impl	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u))$
100	99	adantrlr	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u))$
101	1 3	atncmp	$⊢ (K \in AtLat \land T \in A \land S \in A) \to (\neg T \underset{˙}{\leq} S \leftrightarrow T \neq S)$
102	55 11 56 101	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (\neg T \underset{˙}{\leq} S \leftrightarrow T \neq S)$
103		necom	$⊢ T \neq S \leftrightarrow S \neq T$
104	102 103	bitrdi	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (\neg T \underset{˙}{\leq} S \leftrightarrow S \neq T)$
105	104	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to (\neg T \underset{˙}{\leq} S \leftrightarrow S \neq T)$
106		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to K \in HL$
107		simpl3r	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to T \in A$
108		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to u \in A$
109	68	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to S \in {Base}_{K}$
110	26 1 2 3	hlexch1	$⊢ (K \in HL \land (T \in A \land u \in A \land S \in {Base}_{K}) \land \neg T \underset{˙}{\leq} S) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
111	110	3expia	$⊢ (K \in HL \land (T \in A \land u \in A \land S \in {Base}_{K})) \to (\neg T \underset{˙}{\leq} S \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
112	106 107 108 109 111	syl13anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to (\neg T \underset{˙}{\leq} S \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
113	105 112	sylbird	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \to (S \neq T \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
114	113	imp	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land u \in A) \land S \neq T) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
115	114	an32s	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq T) \land u \in A) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} u) \to u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
116	115	anim2d	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq T) \land u \in A) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)) \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
117	116	reximdva	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq T) \to (\exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
118	117	ad2ant2rl	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T)) \to (\exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
119	118	adantrr	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (\exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} u)) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
120	100 119	mpd	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
121	120	ex	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land S \neq P) \to (((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
122	23 121	pm2.61dane	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \to (((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)))$
123	122	imp	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$

Metamath Proof Explorer

Theorem ps-2

Proof