Metamath Proof Explorer

Theorem djhexmid

Description: Excluded middle property of DVecH vector space closed subspace join. (Contributed by NM, 22-Jul-2014)

Ref Expression
Hypotheses djhexmid.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhexmid.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhexmid.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhexmid.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
djhexmid.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
Assertion djhexmid ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )

Proof

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑋 ∨ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )