Metamath Proof Explorer

Theorem dochpolN

Description: The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dochpol.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochpol.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochpol.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochpol.p ⊢ 𝑃 = ( LPol ‘ 𝑈 )
dochpol.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion dochpolN ( 𝜑 → ⊥ ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 dochpol.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochpol.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochpol.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochpol.p ⊢ 𝑃 = ( LPol ‘ 𝑈 )
5 dochpol.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
7 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
8 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
9 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
10 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
11 3 fvexi ⊢ 𝑈 ∈ V
12 11 a1i ⊢ ( 𝜑 → 𝑈 ∈ V )
13 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
14 1 13 3 6 2 5 dochfN ⊢ ( 𝜑 → ⊥ : 𝒫 ( Base ‘ 𝑈 ) ⟶ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
15 1 3 13 7 dihsslss ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ⊆ ( LSubSp ‘ 𝑈 ) )
16 5 15 syl ⊢ ( 𝜑 → ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ⊆ ( LSubSp ‘ 𝑈 ) )
17 14 16 fssd ⊢ ( 𝜑 → ⊥ : 𝒫 ( Base ‘ 𝑈 ) ⟶ ( LSubSp ‘ 𝑈 ) )
18 1 3 2 6 8 doch1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ ( Base ‘ 𝑈 ) ) = { ( 0g ‘ 𝑈 ) } )
19 5 18 syl ⊢ ( 𝜑 → ( ⊥ ‘ ( Base ‘ 𝑈 ) ) = { ( 0g ‘ 𝑈 ) } )
20 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑥 ⊆ 𝑦 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑥 ⊆ 𝑦 ) ) → 𝑦 ⊆ ( Base ‘ 𝑈 ) )
22 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑥 ⊆ 𝑦 ) ) → 𝑥 ⊆ 𝑦 )
23 1 3 6 2 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) )
24 20 21 22 23 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑥 ⊆ 𝑦 ) ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) )
25 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) )
27 1 3 2 9 10 25 26 dochsatshp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑈 ) )
28 1 3 13 9 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
29 25 26 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
30 1 13 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
31 25 29 30 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
32 6 7 8 9 10 4 12 17 19 24 27 31 islpoldN ⊢ ( 𝜑 → ⊥ ∈ 𝑃 )