Step |
Hyp |
Ref |
Expression |
1 |
|
doch2val2.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
doch2val2.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
doch2val2.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
doch2val2.v |
⊢ 𝑉 = ( Base ‘ 𝑈 ) |
5 |
|
doch2val2.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
doch2val2.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
7 |
|
doch2val2.x |
⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 ) |
8 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
9 |
8 1 2 3 4 5
|
dochval2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) |
10 |
6 7 9
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) |
11 |
10
|
fveq2d |
⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) ) |
12 |
6
|
simpld |
⊢ ( 𝜑 → 𝐾 ∈ HL ) |
13 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
14 |
12 13
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ OP ) |
15 |
|
ssrab2 |
⊢ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ⊆ ran 𝐼 |
16 |
15
|
a1i |
⊢ ( 𝜑 → { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ⊆ ran 𝐼 ) |
17 |
1 2 3 4
|
dih1rn |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 ∈ ran 𝐼 ) |
18 |
6 17
|
syl |
⊢ ( 𝜑 → 𝑉 ∈ ran 𝐼 ) |
19 |
|
sseq2 |
⊢ ( 𝑧 = 𝑉 → ( 𝑋 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑉 ) ) |
20 |
19
|
elrab |
⊢ ( 𝑉 ∈ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ↔ ( 𝑉 ∈ ran 𝐼 ∧ 𝑋 ⊆ 𝑉 ) ) |
21 |
18 7 20
|
sylanbrc |
⊢ ( 𝜑 → 𝑉 ∈ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) |
22 |
21
|
ne0d |
⊢ ( 𝜑 → { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ≠ ∅ ) |
23 |
1 2
|
dihintcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ⊆ ran 𝐼 ∧ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ≠ ∅ ) ) → ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ∈ ran 𝐼 ) |
24 |
6 16 22 23
|
syl12anc |
⊢ ( 𝜑 → ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ∈ ran 𝐼 ) |
25 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
26 |
25 1 2
|
dihcnvcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) |
27 |
6 24 26
|
syl2anc |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) |
28 |
25 8
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) ) |
29 |
14 27 28
|
syl2anc |
⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) ) |
30 |
25 8 1 2 5
|
dochvalr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) ) |
31 |
6 29 30
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) ) |
32 |
25 8
|
opococ |
⊢ ( ( 𝐾 ∈ OP ∧ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) = ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) |
33 |
14 27 32
|
syl2anc |
⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) = ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) |
34 |
33
|
fveq2d |
⊢ ( 𝜑 → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) |
35 |
1 2
|
dihcnvid2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) |
36 |
6 24 35
|
syl2anc |
⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) |
37 |
34 36
|
eqtrd |
⊢ ( 𝜑 → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) ) = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) |
38 |
11 31 37
|
3eqtrd |
⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) |