cdleme22b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 5th line on p. 115. Show that t \/ v =/= p \/ q and s <_ p \/ q implies -. t <_ p \/ q. (Contributed by NM, 2-Dec-2012)

	Ref	Expression
Hypotheses	cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme22.a	$⊢ A = Atoms (K)$
	cdleme22.h	$⊢ H = LHyp (K)$
Assertion	cdleme22b	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme22.a	$⊢ A = Atoms (K)$
5		cdleme22.h	$⊢ H = LHyp (K)$
6		simp1l	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to K \in HL$
7		simp1r1	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \in A$
8		simp1r2	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to T \in A$
9		simp1r3	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \neq T$
10		eqid	$⊢ LLines (K) = LLines (K)$
11	2 4 10	llni2	$⊢ ((K \in HL \land S \in A \land T \in A) \land S \neq T) \to S \underset{˙}{\lor} T \in LLines (K)$
12	6 7 8 9 11	syl31anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\lor} T \in LLines (K)$
13	4 10	llnneat	$⊢ (K \in HL \land S \underset{˙}{\lor} T \in LLines (K)) \to \neg S \underset{˙}{\lor} T \in A$
14	6 12 13	syl2anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg S \underset{˙}{\lor} T \in A$
15		eqid	$⊢ 0. (K) = 0. (K)$
16	15 10	llnn0	$⊢ (K \in HL \land S \underset{˙}{\lor} T \in LLines (K)) \to S \underset{˙}{\lor} T \neq 0. (K)$
17	6 12 16	syl2anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\lor} T \neq 0. (K)$
18	14 17	jca	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (\neg S \underset{˙}{\lor} T \in A \land S \underset{˙}{\lor} T \neq 0. (K))$
19		df-ne	$⊢ S \underset{˙}{\lor} T \neq 0. (K) \leftrightarrow \neg S \underset{˙}{\lor} T = 0. (K)$
20	19	anbi2i	$⊢ (\neg S \underset{˙}{\lor} T \in A \land S \underset{˙}{\lor} T \neq 0. (K)) \leftrightarrow (\neg S \underset{˙}{\lor} T \in A \land \neg S \underset{˙}{\lor} T = 0. (K))$
21		pm4.56	$⊢ (\neg S \underset{˙}{\lor} T \in A \land \neg S \underset{˙}{\lor} T = 0. (K)) \leftrightarrow \neg (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
22	20 21	bitri	$⊢ (\neg S \underset{˙}{\lor} T \in A \land S \underset{˙}{\lor} T \neq 0. (K)) \leftrightarrow \neg (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
23	18 22	sylib	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
24		simp3r2	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
25		simp3l	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to V \in A$
26	1 2 4	hlatlej1	$⊢ (K \in HL \land T \in A \land V \in A) \to T \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
27	6 8 25 26	syl3anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to T \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
28	6	hllatd	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to K \in Lat$
29		eqid	$⊢ {Base}_{K} = {Base}_{K}$
30	29 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
31	7 30	syl	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \in {Base}_{K}$
32	29 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
33	8 32	syl	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to T \in {Base}_{K}$
34	29 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land V \in A) \to T \underset{˙}{\lor} V \in {Base}_{K}$
35	6 8 25 34	syl3anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to T \underset{˙}{\lor} V \in {Base}_{K}$
36	29 1 2	latjle12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land T \in {Base}_{K} \land T \underset{˙}{\lor} V \in {Base}_{K})) \to ((S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land T \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V))$
37	28 31 33 35 36	syl13anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land T \underset{˙}{\leq} (T \underset{˙}{\lor} V)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V))$
38	24 27 37	mpbi2and	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
39	38	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
40		simp3r3	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
41	40	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
42		simpr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
43		simp21	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \in A$
44		simp22	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in A$
45	29 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
46	6 43 44 45	syl3anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
47	29 1 2	latjle12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land T \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
48	28 31 33 46 47	syl13anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
49	48	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
50	41 42 49	mpbi2and	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
51	29 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
52	6 7 8 51	syl3anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
53	29 1 3	latlem12	$⊢ (K \in Lat \land (S \underset{˙}{\lor} T \in {Base}_{K} \land T \underset{˙}{\lor} V \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to (((S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
54	28 52 35 46 53	syl13anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (((S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
55	54	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (((S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
56	39 50 55	mpbi2and	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
57	56	ex	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))$
58		hlop	$⊢ K \in HL \to K \in OP$
59	6 58	syl	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to K \in OP$
60	59	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to K \in OP$
61	52	adantr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
62		simprl	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to (T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A$
63		simprr	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
64	29 1 15 4	leat3	$⊢ ((K \in OP \land S \underset{˙}{\lor} T \in {Base}_{K} \land (T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
65	60 61 62 63 64	syl31anc	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
66	65	exp32	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))))$
67		breq2	$⊢ (T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} 0. (K))$
68	67	biimpa	$⊢ ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} 0. (K)$
69	29 1 15	ople0	$⊢ (K \in OP \land S \underset{˙}{\lor} T \in {Base}_{K}) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} 0. (K) \leftrightarrow S \underset{˙}{\lor} T = 0. (K))$
70	59 52 69	syl2anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} 0. (K) \leftrightarrow S \underset{˙}{\lor} T = 0. (K))$
71	68 70	imbitrid	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} T = 0. (K))$
72	71	imp	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\lor} T = 0. (K)$
73	72	olcd	$⊢ (((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)))) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))$
74	73	exp32	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K))))$
75		simp3r1	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q$
76	2 3 15 4	2atmat0	$⊢ ((K \in HL \land T \in A \land V \in A) \land (P \in A \land Q \in A \land T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q)) \to ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \lor (T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K))$
77	6 8 25 43 44 75 76	syl33anc	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) \in A \lor (T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K))$
78	66 74 77	mpjaod	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K)))$
79	57 78	syld	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (S \underset{˙}{\lor} T \in A \lor S \underset{˙}{\lor} T = 0. (K)))$
80	23 79	mtod	$⊢ ((K \in HL \land (S \in A \land T \in A \land S \neq T)) \land (P \in A \land Q \in A \land P \neq Q) \land (V \in A \land (T \underset{˙}{\lor} V \neq P \underset{˙}{\lor} Q \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem cdleme22b

Proof