Proof of Theorem dihoml4c
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(meet‘𝐾) =
(meet‘𝐾) |
2 | | dihoml4c.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | dihoml4c.i |
. . . 4
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
4 | | dihoml4c.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
5 | | inss1 4120 |
. . . . . 6
⊢ (( ⊥
‘𝑋) ∩ 𝑌) ⊆ ( ⊥ ‘𝑋) |
6 | | dihoml4c.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ran 𝐼) |
7 | | eqid 2738 |
. . . . . . . . 9
⊢
((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊) |
8 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊)) |
9 | 2, 7, 3, 8 | dihrnss 38912 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → 𝑋 ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
10 | 4, 6, 9 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
11 | | dihoml4c.o |
. . . . . . . 8
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
12 | 2, 7, 8, 11 | dochssv 38989 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) → ( ⊥ ‘𝑋) ⊆
(Base‘((DVecH‘𝐾)‘𝑊))) |
13 | 4, 10, 12 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ( ⊥ ‘𝑋) ⊆
(Base‘((DVecH‘𝐾)‘𝑊))) |
14 | 5, 13 | sstrid 3889 |
. . . . 5
⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) |
15 | 2, 3, 7, 8, 11 | dochcl 38987 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( ⊥ ‘𝑋) ∩ 𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) → ( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∈ ran 𝐼) |
16 | 4, 14, 15 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∈ ran 𝐼) |
17 | | dihoml4c.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ran 𝐼) |
18 | 1, 2, 3, 4, 16, 17 | dihmeet2 38980 |
. . 3
⊢ (𝜑 → (◡𝐼‘(( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌)) = ((◡𝐼‘( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)))(meet‘𝐾)(◡𝐼‘𝑌))) |
19 | | eqid 2738 |
. . . . . 6
⊢
(oc‘𝐾) =
(oc‘𝐾) |
20 | 2, 3, 7, 8, 11 | dochcl 38987 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘((DVecH‘𝐾)‘𝑊))) → ( ⊥ ‘𝑋) ∈ ran 𝐼) |
21 | 4, 10, 20 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘𝑋) ∈ ran 𝐼) |
22 | 2, 3 | dihmeetcl 38979 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( ⊥ ‘𝑋) ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼)) → (( ⊥ ‘𝑋) ∩ 𝑌) ∈ ran 𝐼) |
23 | 4, 21, 17, 22 | syl12anc 836 |
. . . . . 6
⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑌) ∈ ran 𝐼) |
24 | 19, 2, 3, 11, 4, 23 | dochvalr3 38997 |
. . . . 5
⊢ (𝜑 → ((oc‘𝐾)‘(◡𝐼‘(( ⊥ ‘𝑋) ∩ 𝑌))) = (◡𝐼‘( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)))) |
25 | 1, 2, 3, 4, 21, 17 | dihmeet2 38980 |
. . . . . . 7
⊢ (𝜑 → (◡𝐼‘(( ⊥ ‘𝑋) ∩ 𝑌)) = ((◡𝐼‘( ⊥ ‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌))) |
26 | 19, 2, 3, 11, 4, 6 | dochvalr3 38997 |
. . . . . . . 8
⊢ (𝜑 → ((oc‘𝐾)‘(◡𝐼‘𝑋)) = (◡𝐼‘( ⊥ ‘𝑋))) |
27 | 26 | oveq1d 7186 |
. . . . . . 7
⊢ (𝜑 → (((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)) = ((◡𝐼‘( ⊥ ‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌))) |
28 | 25, 27 | eqtr4d 2776 |
. . . . . 6
⊢ (𝜑 → (◡𝐼‘(( ⊥ ‘𝑋) ∩ 𝑌)) = (((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌))) |
29 | 28 | fveq2d 6679 |
. . . . 5
⊢ (𝜑 → ((oc‘𝐾)‘(◡𝐼‘(( ⊥ ‘𝑋) ∩ 𝑌))) = ((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))) |
30 | 24, 29 | eqtr3d 2775 |
. . . 4
⊢ (𝜑 → (◡𝐼‘( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌))) = ((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))) |
31 | 30 | oveq1d 7186 |
. . 3
⊢ (𝜑 → ((◡𝐼‘( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)))(meet‘𝐾)(◡𝐼‘𝑌)) = (((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))(meet‘𝐾)(◡𝐼‘𝑌))) |
32 | | dihoml4c.l |
. . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝑌) |
33 | | eqid 2738 |
. . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) |
34 | 33, 2, 3, 4, 6, 17 | dihcnvord 38908 |
. . . . 5
⊢ (𝜑 → ((◡𝐼‘𝑋)(le‘𝐾)(◡𝐼‘𝑌) ↔ 𝑋 ⊆ 𝑌)) |
35 | 32, 34 | mpbird 260 |
. . . 4
⊢ (𝜑 → (◡𝐼‘𝑋)(le‘𝐾)(◡𝐼‘𝑌)) |
36 | 4 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ HL) |
37 | | hloml 36991 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ OML) |
39 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
40 | 39, 2, 3 | dihcnvcl 38905 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘𝑋) ∈ (Base‘𝐾)) |
41 | 4, 6, 40 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (◡𝐼‘𝑋) ∈ (Base‘𝐾)) |
42 | 39, 2, 3 | dihcnvcl 38905 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ ran 𝐼) → (◡𝐼‘𝑌) ∈ (Base‘𝐾)) |
43 | 4, 17, 42 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (◡𝐼‘𝑌) ∈ (Base‘𝐾)) |
44 | 39, 33, 1, 19 | omllaw4 36880 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ (◡𝐼‘𝑋) ∈ (Base‘𝐾) ∧ (◡𝐼‘𝑌) ∈ (Base‘𝐾)) → ((◡𝐼‘𝑋)(le‘𝐾)(◡𝐼‘𝑌) → (((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))(meet‘𝐾)(◡𝐼‘𝑌)) = (◡𝐼‘𝑋))) |
45 | 38, 41, 43, 44 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → ((◡𝐼‘𝑋)(le‘𝐾)(◡𝐼‘𝑌) → (((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))(meet‘𝐾)(◡𝐼‘𝑌)) = (◡𝐼‘𝑋))) |
46 | 35, 45 | mpd 15 |
. . 3
⊢ (𝜑 → (((oc‘𝐾)‘(((oc‘𝐾)‘(◡𝐼‘𝑋))(meet‘𝐾)(◡𝐼‘𝑌)))(meet‘𝐾)(◡𝐼‘𝑌)) = (◡𝐼‘𝑋)) |
47 | 18, 31, 46 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → (◡𝐼‘(( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌)) = (◡𝐼‘𝑋)) |
48 | 2, 3 | dihmeetcl 38979 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼)) → (( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌) ∈ ran 𝐼) |
49 | 4, 16, 17, 48 | syl12anc 836 |
. . 3
⊢ (𝜑 → (( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌) ∈ ran 𝐼) |
50 | 2, 3, 4, 49, 6 | dihcnv11 38909 |
. 2
⊢ (𝜑 → ((◡𝐼‘(( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌)) = (◡𝐼‘𝑋) ↔ (( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)) |
51 | 47, 50 | mpbid 235 |
1
⊢ (𝜑 → (( ⊥ ‘(( ⊥
‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) |