lhp2at0

Description: Join and meet with different atoms under co-atom W . (Contributed by NM, 15-Jun-2013)

	Ref	Expression
Hypotheses	lhp2at0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhp2at0.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhp2at0.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhp2at0.z	$⊢ \underset{˙}{0} = 0. (K)$
	lhp2at0.a	$⊢ A = Atoms (K)$
	lhp2at0.h	$⊢ H = LHyp (K)$
Assertion	lhp2at0	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} V = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lhp2at0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhp2at0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lhp2at0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		lhp2at0.z	$⊢ \underset{˙}{0} = 0. (K)$
5		lhp2at0.a	$⊢ A = Atoms (K)$
6		lhp2at0.h	$⊢ H = LHyp (K)$
7		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in HL$
8		hlol	$⊢ K \in HL \to K \in OL$
9	7 8	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in OL$
10		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \in A$
11		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \in A$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 2 5	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
14	7 10 11 13	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} U \in {Base}_{K}$
15		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to W \in H$
16	12 6	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
17	15 16	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
18		simp3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in A$
19	12 5	atbase	$⊢ V \in A \to V \in {Base}_{K}$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in {Base}_{K}$
21	12 3	latmassOLD	$⊢ (K \in OL \land (P \underset{˙}{\lor} U \in {Base}_{K} \land W \in {Base}_{K} \land V \in {Base}_{K})) \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} W) \underset{˙}{\land} V = (P \underset{˙}{\lor} U) \underset{˙}{\land} (W \underset{˙}{\land} V)$
22	9 14 17 20 21	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} W) \underset{˙}{\land} V = (P \underset{˙}{\lor} U) \underset{˙}{\land} (W \underset{˙}{\land} V)$
23	1 3 4 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = \underset{˙}{0}$
24	23	3adant3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \to P \underset{˙}{\land} W = \underset{˙}{0}$
25	24	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = \underset{˙}{0}$
26	25	oveq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = \underset{˙}{0} \underset{˙}{\lor} U$
27	12 5	atbase	$⊢ U \in A \to U \in {Base}_{K}$
28	11 27	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \in {Base}_{K}$
29		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \underset{˙}{\leq} W$
30	12 1 2 3 5	atmod4i2	$⊢ (K \in HL \land (P \in A \land U \in {Base}_{K} \land W \in {Base}_{K}) \land U \underset{˙}{\leq} W) \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = (P \underset{˙}{\lor} U) \underset{˙}{\land} W$
31	7 10 28 17 29 30	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = (P \underset{˙}{\lor} U) \underset{˙}{\land} W$
32	12 2 4	olj02	$⊢ (K \in OL \land U \in {Base}_{K}) \to \underset{˙}{0} \underset{˙}{\lor} U = U$
33	9 28 32	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to \underset{˙}{0} \underset{˙}{\lor} U = U$
34	26 31 33	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
35	34	oveq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} W) \underset{˙}{\land} V = U \underset{˙}{\land} V$
36	22 35	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} (W \underset{˙}{\land} V) = U \underset{˙}{\land} V$
37		simp3r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \underset{˙}{\leq} W$
38	7	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in Lat$
39	12 1 3	latleeqm2	$⊢ (K \in Lat \land V \in {Base}_{K} \land W \in {Base}_{K}) \to (V \underset{˙}{\leq} W \leftrightarrow W \underset{˙}{\land} V = V)$
40	38 20 17 39	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (V \underset{˙}{\leq} W \leftrightarrow W \underset{˙}{\land} V = V)$
41	37 40	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to W \underset{˙}{\land} V = V$
42	41	oveq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} (W \underset{˙}{\land} V) = (P \underset{˙}{\lor} U) \underset{˙}{\land} V$
43		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \neq V$
44		hlatl	$⊢ K \in HL \to K \in AtLat$
45	7 44	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in AtLat$
46	3 4 5	atnem0	$⊢ (K \in AtLat \land U \in A \land V \in A) \to (U \neq V \leftrightarrow U \underset{˙}{\land} V = \underset{˙}{0})$
47	45 11 18 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (U \neq V \leftrightarrow U \underset{˙}{\land} V = \underset{˙}{0})$
48	43 47	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \underset{˙}{\land} V = \underset{˙}{0}$
49	36 42 48	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} V = \underset{˙}{0}$

Metamath Proof Explorer

Theorem lhp2at0

Proof