1cvrat

Description: Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 30-Apr-2012)

	Ref	Expression
Hypotheses	1cvrat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	1cvrat.l	⊢ ≤ = ( le ‘ 𝐾 )
	1cvrat.j	⊢ ∨ = ( join ‘ 𝐾 )
	1cvrat.m	⊢ ∧ = ( meet ‘ 𝐾 )
	1cvrat.u	⊢ 1 = ( 1. ‘ 𝐾 )
	1cvrat.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	1cvrat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	1cvrat	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1cvrat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		1cvrat.l	⊢ ≤ = ( le ‘ 𝐾 )
3		1cvrat.j	⊢ ∨ = ( join ‘ 𝐾 )
4		1cvrat.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		1cvrat.u	⊢ 1 = ( 1. ‘ 𝐾 )
6		1cvrat.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
7		1cvrat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9	8	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
10		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
11	1 7	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
12	10 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
13		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐴 )
14	1 7	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
15	13 14	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐵 )
16	1 3	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
17	9 12 15 16	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
18	17	oveq1d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) )
19	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 )
20	9 15 12 19	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 )
21		simp23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
22	1 4	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
23	9 20 21 22	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
24	18 23	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
25		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
26	21 13 10	3jca	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
27		simp31	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑄 )
28	27	necomd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≠ 𝑃 )
29		simp33	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑋 )
30		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
31	30	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ OP )
32	1 2 5	ople1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ≤ 1 )
33	31 15 32	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≤ 1 )
34		simp32	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑋 𝐶 1 )
35	1 2 3 5 6 7	1cvrjat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑃 ) = 1 )
36	25 21 10 34 29 35	syl32anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑃 ) = 1 )
37	33 36	breqtrrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) )
38	1 2 3 4 7	cvrat3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 ) )
39	38	imp	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) ∧ ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 )
40	25 26 28 29 37 39	syl23anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 )
41	24 40	eqeltrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )

Metamath Proof Explorer

Theorem 1cvrat

Proof