cdleme42c

Description: Part of proof of Lemma E in Crawley p. 113. Match -. x .<_ W . (Contributed by NM, 6-Mar-2013)

	Ref	Expression
Hypotheses	cdleme42.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdleme42.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme42.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme42.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme42.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme42.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme42.v	⊢ 𝑉 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
Assertion	cdleme42c	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ¬ ( 𝑅 ∨ 𝑉 ) ≤ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		cdleme42.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdleme42.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdleme42.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdleme42.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdleme42.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdleme42.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdleme42.v	⊢ 𝑉 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
8		simp2r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ¬ 𝑅 ≤ 𝑊 )
9		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
10	9	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
11		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐴 )
12	1 5	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
13	11 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐵 )
14		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ 𝐴 )
15	1 3 5	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
16	9 11 14 15	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 )
17		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
18	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
19	17 18	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
20	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑆 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
21	10 16 19 20	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
22	7 21	eqeltrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑉 ∈ 𝐵 )
23	1 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑅 ∨ 𝑉 ) ≤ 𝑊 ) )
24	10 13 22 19 23	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑅 ∨ 𝑉 ) ≤ 𝑊 ) )
25		simpl	⊢ ( ( 𝑅 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) → 𝑅 ≤ 𝑊 )
26	24 25	syl6bir	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑉 ) ≤ 𝑊 → 𝑅 ≤ 𝑊 ) )
27	8 26	mtod	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ¬ ( 𝑅 ∨ 𝑉 ) ≤ 𝑊 )

Metamath Proof Explorer

Theorem cdleme42c

Proof