Step |
Hyp |
Ref |
Expression |
1 |
|
arglem1.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
2 |
|
arglem1.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
3 |
|
arglem1.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
arglem1.f |
⊢ 𝐹 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) |
5 |
|
arglem1.g |
⊢ 𝐺 = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) |
6 |
|
simpl11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐾 ∈ HL ) |
7 |
6
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐾 ∈ Lat ) |
8 |
|
simpl12 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 ) |
9 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
10 |
9 3
|
atbase |
⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
11 |
8 10
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
12 |
|
simpl13 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 ) |
13 |
9 3
|
atbase |
⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) ) |
14 |
12 13
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) ) |
15 |
|
simpl21 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ∈ 𝐴 ) |
16 |
9 3
|
atbase |
⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) ) |
17 |
15 16
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) ) |
18 |
|
simpl22 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑇 ∈ 𝐴 ) |
19 |
9 3
|
atbase |
⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) ) |
20 |
18 19
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑇 ∈ ( Base ‘ 𝐾 ) ) |
21 |
9 1
|
latj4 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ) |
22 |
7 11 14 17 20 21
|
syl122anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ) |
23 |
|
simpr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐺 ∈ 𝐴 ) |
24 |
5 23
|
eqeltrrid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 ) |
25 |
|
simpl31 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ≠ 𝑆 ) |
26 |
|
eqid |
⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 ) |
27 |
1 3 26
|
llni2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑆 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) |
28 |
6 8 15 25 27
|
syl31anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) |
29 |
|
simpl32 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ≠ 𝑇 ) |
30 |
1 3 26
|
llni2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑇 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) |
31 |
6 12 18 29 30
|
syl31anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) |
32 |
|
eqid |
⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 ) |
33 |
1 2 3 26 32
|
2llnmj |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) ) |
34 |
6 28 31 33
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) ) |
35 |
24 34
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) |
36 |
22 35
|
eqeltrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) |
37 |
|
simpl23 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ≠ 𝑄 ) |
38 |
1 3 26
|
llni2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ) |
39 |
6 8 12 37 38
|
syl31anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ) |
40 |
|
simpl33 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ≠ 𝑇 ) |
41 |
1 3 26
|
llni2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ 𝑆 ≠ 𝑇 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) |
42 |
6 15 18 40 41
|
syl31anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) |
43 |
1 2 3 26 32
|
2llnmj |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) ) |
44 |
6 39 42 43
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) ) |
45 |
36 44
|
mpbird |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 ) |
46 |
4 45
|
eqeltrid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐹 ∈ 𝐴 ) |