Metamath Proof Explorer

Theorem dochsnkr2cl

Description: The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015)

Ref Expression
Hypotheses dochsnkr2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsnkr2.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsnkr2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsnkr2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochsnkr2.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochsnkr2.a ⊢ + = ( +g ‘ 𝑈 )
dochsnkr2.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
dochsnkr2.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochsnkr2.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
dochsnkr2.r ⊢ 𝑅 = ( Base ‘ 𝐷 )
dochsnkr2.g ⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
dochsnkr2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsnkr2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion dochsnkr2cl ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 dochsnkr2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsnkr2.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsnkr2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsnkr2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochsnkr2.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 dochsnkr2.a ⊢ + = ( +g ‘ 𝑈 )
7 dochsnkr2.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
8 dochsnkr2.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
9 dochsnkr2.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
10 dochsnkr2.r ⊢ 𝑅 = ( Base ‘ 𝐷 )
11 dochsnkr2.g ⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
12 dochsnkr2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 dochsnkr2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14 1 3 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
15 13 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
16 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
17 4 16 lspsnid ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
18 14 15 17 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 dochsnkr2 ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )
20 15 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
21 1 3 2 4 16 12 20 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
22 19 21 eqtr4d ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
23 22 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) )
24 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
25 1 3 4 16 24 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 12 15 25 syl2anc ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 24 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
28 12 26 27 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
29 23 28 eqtr2d ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
30 18 29 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
31 eldifsni ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
32 13 31 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
33 eldifsn ⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑋 ≠ 0 ) )
34 30 32 33 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )