Proof of Theorem djhlj
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simprl 771 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
3 | | djhlj.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
4 | | djhlj.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | djhlj.i |
. . . . 5
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
6 | | eqid 2738 |
. . . . 5
⊢
((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊) |
7 | | eqid 2738 |
. . . . 5
⊢
(Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊)) |
8 | 3, 4, 5, 6, 7 | dihss 38888 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
9 | 2, 8 | syldan 594 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
10 | | simprr 773 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
11 | 3, 4, 5, 6, 7 | dihss 38888 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
12 | 10, 11 | syldan 594 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
13 | | eqid 2738 |
. . . 4
⊢
((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊) |
14 | | djhlj.j |
. . . 4
⊢ 𝐽 = ((joinH‘𝐾)‘𝑊) |
15 | 4, 6, 7, 13, 14 | djhval 39035 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)) ∧ (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocH‘𝐾)‘𝑊)‘((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
16 | 1, 9, 12, 15 | syl12anc 836 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocH‘𝐾)‘𝑊)‘((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
17 | | hlop 36999 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
18 | 17 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ OP) |
19 | | eqid 2738 |
. . . . . . . 8
⊢
(oc‘𝐾) =
(oc‘𝐾) |
20 | 3, 19 | opoccl 36831 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
21 | 18, 2, 20 | syl2anc 587 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) |
22 | 3, 19 | opoccl 36831 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) |
23 | 18, 10, 22 | syl2anc 587 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) |
24 | | eqid 2738 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
25 | 3, 24, 4, 5 | dihmeet 38980 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝐼‘((oc‘𝐾)‘𝑋)) ∩ (𝐼‘((oc‘𝐾)‘𝑌)))) |
26 | 1, 21, 23, 25 | syl3anc 1372 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((𝐼‘((oc‘𝐾)‘𝑋)) ∩ (𝐼‘((oc‘𝐾)‘𝑌)))) |
27 | 3, 19, 4, 5, 13 | dochvalr2 38999 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) = (𝐼‘((oc‘𝐾)‘𝑋))) |
28 | 2, 27 | syldan 594 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) = (𝐼‘((oc‘𝐾)‘𝑋))) |
29 | 3, 19, 4, 5, 13 | dochvalr2 38999 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌)) = (𝐼‘((oc‘𝐾)‘𝑌))) |
30 | 10, 29 | syldan 594 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌)) = (𝐼‘((oc‘𝐾)‘𝑌))) |
31 | 28, 30 | ineq12d 4104 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌))) = ((𝐼‘((oc‘𝐾)‘𝑋)) ∩ (𝐼‘((oc‘𝐾)‘𝑌)))) |
32 | 26, 31 | eqtr4d 2776 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = ((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌)))) |
33 | 32 | fveq2d 6678 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (((ocH‘𝐾)‘𝑊)‘((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
34 | | hllat 37000 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
35 | 34 | ad2antrr 726 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ Lat) |
36 | 3, 24 | latmcl 17778 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) |
37 | 35, 21, 23, 36 | syl3anc 1372 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) |
38 | 3, 19, 4, 5, 13 | dochvalr2 38999 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝐼‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))))) |
39 | 37, 38 | syldan 594 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((ocH‘𝐾)‘𝑊)‘(𝐼‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝐼‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))))) |
40 | 33, 39 | eqtr3d 2775 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((ocH‘𝐾)‘𝑊)‘((((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocH‘𝐾)‘𝑊)‘(𝐼‘𝑌)))) = (𝐼‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))))) |
41 | | hlol 36998 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
42 | 41 | ad2antrr 726 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ OL) |
43 | | djhlj.k |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
44 | 3, 43, 24, 19 | oldmm4 36857 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 ∨ 𝑌)) |
45 | 42, 2, 10, 44 | syl3anc 1372 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋 ∨ 𝑌)) |
46 | 45 | fveq2d 6678 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))) = (𝐼‘(𝑋 ∨ 𝑌))) |
47 | 16, 40, 46 | 3eqtrrd 2778 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) |