lhpmcvr5N

Description: Specialization of lhpmcvr2 . (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lhpmcvr2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lhpmcvr2.l	⊢ ≤ = ( le ‘ 𝐾 )
	lhpmcvr2.j	⊢ ∨ = ( join ‘ 𝐾 )
	lhpmcvr2.m	⊢ ∧ = ( meet ‘ 𝐾 )
	lhpmcvr2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhpmcvr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpmcvr5N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lhpmcvr2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lhpmcvr2.l	⊢ ≤ = ( le ‘ 𝐾 )
3		lhpmcvr2.j	⊢ ∨ = ( join ‘ 𝐾 )
4		lhpmcvr2.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		lhpmcvr2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		lhpmcvr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7	1 2 3 4 5 6	lhpmcvr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
8	7	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
9		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ 𝑝 ≤ 𝑊 )
10		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
12		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑝 ∈ 𝐴 )
13	12 9	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) )
14		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑌 ∈ 𝐵 )
15		simp13r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
16		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
17	16	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
18	1 5	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
19	18	3ad2ant2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑝 ∈ 𝐵 )
20		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
21		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
22	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
23	21 22	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
24	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
25	17 20 23 24	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
26	1 2 3	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → 𝑝 ≤ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) )
27	17 19 25 26	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑝 ≤ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) )
28		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
29	27 28	breqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑝 ≤ 𝑋 )
30	1 2 3 4 5 6	lhpmcvr4N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑝 ≤ 𝑋 ) ) → ¬ 𝑝 ≤ 𝑌 )
31	10 11 13 14 15 29 30	syl123anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ 𝑝 ≤ 𝑌 )
32	9 31 28	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
33	32	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) )
34	33	reximdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) )
35	8 34	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ ( 𝑝 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )

Metamath Proof Explorer

Theorem lhpmcvr5N

Proof