cvrat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 30-Nov-2011)

	Ref	Expression
Hypotheses	cvrat2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrat2.j	⊢ ∨ = ( join ‘ 𝐾 )
	cvrat2.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	cvrat2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	cvrat2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cvrat2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrat2.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cvrat2.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		cvrat2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6	1 2 5 3 4	atcvrj0	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 = ( 0. ‘ 𝐾 ) ↔ 𝑃 = 𝑄 ) )
7	6	3expa	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 = ( 0. ‘ 𝐾 ) ↔ 𝑃 = 𝑄 ) )
8	7	necon3bid	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ↔ 𝑃 ≠ 𝑄 ) )
9		simpl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
10		simpr1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
11		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
12	11	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
13		simpr2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
14	1 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
15	13 14	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐵 )
16		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
17	1 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
18	16 17	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
19	1 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
20	12 15 18 19	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
21		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
22	1 21 3	cvrlt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
23	22	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
24	9 10 20 23	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
25	1 21 2 5 4	cvrat	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ∧ 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ 𝐴 ) )
26	25	expcomd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋 ∈ 𝐴 ) ) )
27	24 26	syld	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋 ∈ 𝐴 ) ) )
28	27	imp	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋 ∈ 𝐴 ) )
29	8 28	sylbird	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ≠ 𝑄 → 𝑋 ∈ 𝐴 ) )
30	29	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) → ( 𝑃 ≠ 𝑄 → 𝑋 ∈ 𝐴 ) ) )
31	30	com23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ≠ 𝑄 → ( 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) → 𝑋 ∈ 𝐴 ) ) )
32	31	impd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ 𝐴 ) )
33	32	3impia	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ∈ 𝐴 )

Metamath Proof Explorer

Theorem cvrat2

Proof