Theorem islpln2a

Description: The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012)

	Ref	Expression
Hypotheses	islpln2a.l	⊢ ≤ = ( le ‘ 𝐾 )
	islpln2a.j	⊢ ∨ = ( join ‘ 𝐾 )
	islpln2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	islpln2a.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	islpln2a	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islpln2a.l	⊢ ≤ = ( le ‘ 𝐾 )
2		islpln2a.j	⊢ ∨ = ( join ‘ 𝐾 )
3		islpln2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		islpln2a.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5		oveq1	⊢ ( 𝑄 = 𝑅 → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑅 ) )
6	2 3	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
7	6	3ad2antr2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
8	5 7	sylan9eqr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑄 ∨ 𝑅 ) = 𝑅 )
9	8	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑅 ∨ 𝑆 ) )
10		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝐾 ∈ HL )
11		simplr2	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝑅 ∈ 𝐴 )
12		simplr3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝑆 ∈ 𝐴 )
13	2 3 4	2atnelpln	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝑃 )
14	10 11 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝑃 )
15	9 14	eqneltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
16	15	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 = 𝑅 → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
17	16	necon2ad	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → 𝑄 ≠ 𝑅 ) )
18		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
19	18	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
20		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
21		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22	21 3	atbase	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
23	20 22	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
24	21 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
25	24	3adant3r3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
26	21 1 2	latleeqj2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) ) )
27	19 23 25 26	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) ) )
28	2 3 4	2atnelpln	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )
29	28	3adant3r3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )
30		eleq1	⊢ ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) )
31	30	notbid	⊢ ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ( ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) )
32	29 31	syl5ibrcom	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
33	27 32	sylbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
34	33	con2d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
35	17 34	jcad	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
36	1 2 3 4	lplni2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
37	36	3expia	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
38	35 37	impbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )