Step | Hyp | Ref
| Expression |
1 | | ssintub 4430 |
. 2
⊢ 𝑋 ⊆ ∩ {𝑧
∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} |
2 | | dochss.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | eqid 2610 |
. . . . 5
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
4 | | dochss.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | dochss.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑈) |
6 | | dochss.o |
. . . . 5
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
7 | 2, 3, 4, 5, 6 | dochcl 35660 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
8 | | eqid 2610 |
. . . . 5
⊢
(oc‘𝐾) =
(oc‘𝐾) |
9 | 8, 2, 3, 6 | dochvalr 35664 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘𝑋)) =
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋))))) |
10 | 7, 9 | syldan 486 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘( ⊥
‘𝑋)) =
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋))))) |
11 | 8, 2, 3, 4, 5, 6 | dochval2 35659 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) = (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})))) |
12 | 11 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋)) = (◡((DIsoH‘𝐾)‘𝑊)‘(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))))) |
13 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
15 | 13, 2, 3, 4, 14 | dihf11 35574 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
17 | | f1f1orn 6061 |
. . . . . . . . 9
⊢
(((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
19 | | hlop 33667 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
20 | 19 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝐾 ∈ OP) |
21 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
22 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ⊆ ran ((DIsoH‘𝐾)‘𝑊) |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ⊆ ran ((DIsoH‘𝐾)‘𝑊)) |
24 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(1.‘𝐾) =
(1.‘𝐾) |
25 | 24, 2, 3, 4, 5 | dih1 35593 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((DIsoH‘𝐾)‘𝑊)‘(1.‘𝐾)) = 𝑉) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (((DIsoH‘𝐾)‘𝑊)‘(1.‘𝐾)) = 𝑉) |
27 | | f1fn 6015 |
. . . . . . . . . . . . . . . 16
⊢
(((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈) → ((DIsoH‘𝐾)‘𝑊) Fn (Base‘𝐾)) |
28 | 16, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((DIsoH‘𝐾)‘𝑊) Fn (Base‘𝐾)) |
29 | 13, 24 | op1cl 33490 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ OP →
(1.‘𝐾) ∈
(Base‘𝐾)) |
30 | 20, 29 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (1.‘𝐾) ∈ (Base‘𝐾)) |
31 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . 15
⊢
((((DIsoH‘𝐾)‘𝑊) Fn (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) → (((DIsoH‘𝐾)‘𝑊)‘(1.‘𝐾)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
32 | 28, 30, 31 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (((DIsoH‘𝐾)‘𝑊)‘(1.‘𝐾)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
33 | 26, 32 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑉 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
34 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑋 ⊆ 𝑉) |
35 | | sseq2 3590 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑉 → (𝑋 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑉)) |
36 | 35 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ↔ (𝑉 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∧ 𝑋 ⊆ 𝑉)) |
37 | 33, 34, 36 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑉 ∈ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) |
38 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} → {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ≠ ∅) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ≠ ∅) |
40 | 2, 3 | dihintcl 35651 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ({𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ⊆ ran ((DIsoH‘𝐾)‘𝑊) ∧ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ≠ ∅)) → ∩ {𝑧
∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
41 | 21, 23, 39, 40 | syl12anc 1316 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
42 | | f1ocnvdm 6440 |
. . . . . . . . . 10
⊢
((((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊) ∧ ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) |
43 | 18, 41, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) |
44 | 13, 8 | opoccl 33499 |
. . . . . . . . 9
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾)) |
45 | 20, 43, 44 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾)) |
46 | | f1ocnvfv1 6432 |
. . . . . . . 8
⊢
((((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊) ∧ ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) ∈ (Base‘𝐾)) → (◡((DIsoH‘𝐾)‘𝑊)‘(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})))) = ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) |
47 | 18, 45, 46 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (◡((DIsoH‘𝐾)‘𝑊)‘(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})))) = ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) |
48 | 12, 47 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋)) = ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) |
49 | 48 | fveq2d 6107 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋))) = ((oc‘𝐾)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})))) |
50 | 13, 8 | opococ 33500 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) = (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) |
51 | 20, 43, 50 | syl2anc 691 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((oc‘𝐾)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) = (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) |
52 | 49, 51 | eqtrd 2644 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋))) = (◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) |
53 | 52 | fveq2d 6107 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘𝑋)))) = (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}))) |
54 | | f1ocnvfv2 6433 |
. . . 4
⊢
((((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊) ∧ ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) = ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) |
55 | 18, 41, 54 | syl2anc 691 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧})) = ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧}) |
56 | 10, 53, 55 | 3eqtrrd 2649 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ∩ {𝑧 ∈ ran ((DIsoH‘𝐾)‘𝑊) ∣ 𝑋 ⊆ 𝑧} = ( ⊥ ‘( ⊥
‘𝑋))) |
57 | 1, 56 | syl5sseq 3616 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋))) |