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 ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ( 𝑋 ) ) = 𝑉 )