cdleme22d

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-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	cdleme22d	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$

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		simp3r	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in HL$
8		simp22l	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \in A$
9		simp23l	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \in A$
10	1 2 4	hlatlej1	$⊢ (K \in HL \land T \in A \land V \in A) \to T \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
12	7	hllatd	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in Lat$
13		simp21l	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
16	13 15	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \in {Base}_{K}$
17	14 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
18	8 17	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \in {Base}_{K}$
19	14 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land V \in A) \to T \underset{˙}{\lor} V \in {Base}_{K}$
20	7 8 9 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \underset{˙}{\lor} V \in {Base}_{K}$
21	14 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))$
22	12 16 18 20 21	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \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))$
23	6 11 22	mpbi2and	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V)$
24	14 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
25	7 13 8 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
26		simp1r	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to W \in H$
27	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
28	26 27	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to W \in {Base}_{K}$
29	14 1 3	latmlem1	$⊢ (K \in Lat \land (S \underset{˙}{\lor} T \in {Base}_{K} \land T \underset{˙}{\lor} V \in {Base}_{K} \land W \in {Base}_{K})) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} W))$
30	12 25 20 28 29	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (T \underset{˙}{\lor} V) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} W))$
31	23 30	mpd	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} ((T \underset{˙}{\lor} V) \underset{˙}{\land} W)$
32		simp1	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (K \in HL \land W \in H)$
33		simp22	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
34		eqid	$⊢ 0. (K) = 0. (K)$
35	1 3 34 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \to T \underset{˙}{\land} W = 0. (K)$
36	32 33 35	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to T \underset{˙}{\land} W = 0. (K)$
37	36	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (T \underset{˙}{\land} W) \underset{˙}{\lor} V = 0. (K) \underset{˙}{\lor} V$
38		simp23r	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \underset{˙}{\leq} W$
39	14 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (V \in A \land T \in {Base}_{K} \land W \in {Base}_{K}) \land V \underset{˙}{\leq} W) \to (T \underset{˙}{\land} W) \underset{˙}{\lor} V = (T \underset{˙}{\lor} V) \underset{˙}{\land} W$
40	7 9 18 28 38 39	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (T \underset{˙}{\land} W) \underset{˙}{\lor} V = (T \underset{˙}{\lor} V) \underset{˙}{\land} W$
41		hlol	$⊢ K \in HL \to K \in OL$
42	7 41	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in OL$
43	14 4	atbase	$⊢ V \in A \to V \in {Base}_{K}$
44	9 43	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V \in {Base}_{K}$
45	14 2 34	olj02	$⊢ (K \in OL \land V \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} V = V$
46	42 44 45	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to 0. (K) \underset{˙}{\lor} V = V$
47	37 40 46	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (T \underset{˙}{\lor} V) \underset{˙}{\land} W = V$
48	31 47	breqtrd	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} V$
49		hlatl	$⊢ K \in HL \to K \in AtLat$
50	7 49	syl	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to K \in AtLat$
51		simp21r	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to \neg S \underset{˙}{\leq} W$
52		simp3l	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to S \neq T$
53	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land S \neq T)) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A$
54	7 26 13 51 8 52 53	syl222anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A$
55	1 4	atcmp	$⊢ (K \in AtLat \land (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A \land V \in A) \to (((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} V \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} W = V)$
56	50 54 9 55	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\leq} V \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} W = V)$
57	48 56	mpbid	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W = V$
58	57	eqcomd	$⊢ ((K \in HL \land W \in H) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq T \land S \underset{˙}{\leq} (T \underset{˙}{\lor} V))) \to V = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdleme22d

Proof