Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochsnkr2 Structured version   Visualization version   GIF version

Theorem dochsnkr2 35780
 Description: Kernel of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkr 33422. (Contributed by NM, 27-Oct-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dochsnkr2 (𝜑 → (𝐿𝐺) = ( ‘{𝑋}))
Distinct variable groups:   𝑣,𝑘,𝑤, +   𝐷,𝑘   ,𝑘,𝑣,𝑤   𝑅,𝑘,𝑣   · ,𝑘,𝑣,𝑤   𝑣,𝑉   𝑘,𝑋,𝑣,𝑤
Allowed substitution hints:   𝜑(𝑤,𝑣,𝑘)   𝐷(𝑤,𝑣)   𝑅(𝑤)   𝑈(𝑤,𝑣,𝑘)   𝐺(𝑤,𝑣,𝑘)   𝐻(𝑤,𝑣,𝑘)   𝐾(𝑤,𝑣,𝑘)   𝐿(𝑤,𝑣,𝑘)   𝑉(𝑤,𝑘)   𝑊(𝑤,𝑣,𝑘)   0 (𝑤,𝑣,𝑘)

Proof of Theorem dochsnkr2
StepHypRef Expression
1 dochsnkr2.v . 2 𝑉 = (Base‘𝑈)
2 dochsnkr2.a . 2 + = (+g𝑈)
3 eqid 2610 . 2 (LSpan‘𝑈) = (LSpan‘𝑈)
4 eqid 2610 . 2 (LSSum‘𝑈) = (LSSum‘𝑈)
5 eqid 2610 . 2 (LSHyp‘𝑈) = (LSHyp‘𝑈)
6 dochsnkr2.h . . 3 𝐻 = (LHyp‘𝐾)
7 dochsnkr2.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
8 dochsnkr2.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
96, 7, 8dvhlvec 35416 . 2 (𝜑𝑈 ∈ LVec)
10 dochsnkr2.o . . 3 = ((ocH‘𝐾)‘𝑊)
11 dochsnkr2.z . . 3 0 = (0g𝑈)
12 dochsnkr2.x . . 3 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
136, 10, 7, 1, 11, 5, 8, 12dochsnshp 35760 . 2 (𝜑 → ( ‘{𝑋}) ∈ (LSHyp‘𝑈))