Step |
Hyp |
Ref |
Expression |
1 |
|
2llnmj.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
2 |
|
2llnmj.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
3 |
|
2llnmj.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
2llnmj.n |
⊢ 𝑁 = ( LLines ‘ 𝐾 ) |
5 |
|
2llnmj.p |
⊢ 𝑃 = ( LPlanes ‘ 𝐾 ) |
6 |
|
simp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝐾 ∈ HL ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
8 |
7 4
|
llnbase |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
9 |
8
|
3ad2ant2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
10 |
7 4
|
llnbase |
⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
11 |
10
|
3ad2ant3 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
12 |
|
eqid |
⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 ) |
13 |
7 1 2 12
|
cvrexch |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) |
14 |
6 9 11 13
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) |
15 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ HL ) |
16 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) |
17 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑌 ∈ 𝑁 ) |
18 |
|
hllat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat ) |
19 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
20 |
7 19 2
|
latmle2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) |
21 |
18 8 10 20
|
syl3an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) |
22 |
21
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) |
23 |
19 12 3 4
|
atcvrlln2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) |
24 |
15 16 17 22 23
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) |
25 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ 𝑁 ) |
26 |
7 2
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
27 |
18 8 10 26
|
syl3an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
28 |
6 27 11
|
3jca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) |
29 |
7 12 3 4
|
atcvrlln |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ 𝑌 ∈ 𝑁 ) ) |
30 |
28 29
|
sylan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ 𝑌 ∈ 𝑁 ) ) |
31 |
25 30
|
mpbird |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) |
32 |
24 31
|
impbida |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) ) |
33 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) → 𝐾 ∈ HL ) |
34 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) → 𝑋 ∈ 𝑁 ) |
35 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) |
36 |
7 19 1
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) |
37 |
18 8 10 36
|
syl3an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) |
38 |
37
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) |
39 |
19 12 4 5
|
llncvrlpln2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) |
40 |
33 34 35 38 39
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) |
41 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → 𝑋 ∈ 𝑁 ) |
42 |
7 1
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
43 |
18 8 10 42
|
syl3an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝑋 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
44 |
6 9 43
|
3jca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ) |
45 |
7 12 4 5
|
llncvrlpln |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) ) |
46 |
44 45
|
sylan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) ) |
47 |
41 46
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) |
48 |
40 47
|
impbida |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ) ) |
49 |
14 32 48
|
3bitr4d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ ( 𝑋 ∨ 𝑌 ) ∈ 𝑃 ) ) |