Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemefrs29.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cdlemefrs29.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
cdlemefrs29.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
4 |
|
cdlemefrs29.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
5 |
|
cdlemefrs29.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
6 |
|
cdlemefrs29.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
7 |
|
cdlemefrs29.eq |
⊢ ( 𝑠 = 𝑅 → ( 𝜑 ↔ 𝜓 ) ) |
8 |
|
anass |
⊢ ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝜑 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) ) |
9 |
|
simpl3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → 𝜓 ) |
10 |
7
|
pm5.32ri |
⊢ ( ( 𝜑 ∧ 𝑠 = 𝑅 ) ↔ ( 𝜓 ∧ 𝑠 = 𝑅 ) ) |
11 |
10
|
baibr |
⊢ ( 𝜓 → ( 𝑠 = 𝑅 ↔ ( 𝜑 ∧ 𝑠 = 𝑅 ) ) ) |
12 |
9 11
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 = 𝑅 ↔ ( 𝜑 ∧ 𝑠 = 𝑅 ) ) ) |
13 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
14 |
2 4 13 5 6
|
lhpmat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) ) |
15 |
14
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) → ( 𝑅 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) ) |
16 |
15
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑅 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) ) |
17 |
16
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) ) |
18 |
|
simpl1l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → 𝐾 ∈ HL ) |
19 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
20 |
18 19
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → 𝐾 ∈ OL ) |
21 |
1 5
|
atbase |
⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵 ) |
22 |
21
|
adantl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐵 ) |
23 |
1 3 13
|
olj01 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑠 ∈ 𝐵 ) → ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) = 𝑠 ) |
24 |
20 22 23
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) = 𝑠 ) |
25 |
17 24
|
eqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑠 ) |
26 |
25
|
eqeq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ↔ 𝑠 = 𝑅 ) ) |
27 |
26
|
anbi2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝜑 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( 𝜑 ∧ 𝑠 = 𝑅 ) ) ) |
28 |
12 26 27
|
3bitr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ↔ ( 𝜑 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) ) |
29 |
28
|
anbi2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝜑 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) ) ) |
30 |
8 29
|
bitr4id |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝜓 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) ) |