Step |
Hyp |
Ref |
Expression |
1 |
|
djhexmid.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
djhexmid.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
djhexmid.v |
⊢ 𝑉 = ( Base ‘ 𝑈 ) |
4 |
|
djhexmid.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
djhexmid.j |
⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
simpl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
7 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ⊆ 𝑉 ) |
8 |
1 2 3 4
|
dochssv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) |
9 |
1 2 3 4 5
|
djhval |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) |
10 |
6 7 8 9
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) ) |
11 |
|
eqid |
⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 ) |
12 |
1 2 3 11 4
|
dochlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
13 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
14 |
1 2 11 13 4
|
dochnoncon |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = { ( 0g ‘ 𝑈 ) } ) |
15 |
12 14
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = { ( 0g ‘ 𝑈 ) } ) |
16 |
1 2 4 3 13
|
doch1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑈 ) } ) |
17 |
16
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑈 ) } ) |
18 |
15 17
|
eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑉 ) ) |
19 |
18
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) ) |
20 |
|
eqid |
⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
21 |
1 20 2 3
|
dih1rn |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
22 |
21
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
23 |
1 20 4
|
dochoc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 ) |
24 |
22 23
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 ) |
25 |
10 19 24
|
3eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) |