Home | Metamath
Proof Explorer Theorem List (p. 387 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dochexmidlem4 38601 | Lemma for dochexmid 38606. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ (𝜑 → 𝑞 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → 𝑞 ⊆ (( ⊥ ‘𝑋) ∩ 𝑀)) ⇒ ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | ||
Theorem | dochexmidlem5 38602 | Lemma for dochexmid 38606. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ∩ 𝑀) = { 0 }) | ||
Theorem | dochexmidlem6 38603 | Lemma for dochexmid 38606. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 = 𝑋) | ||
Theorem | dochexmidlem7 38604 | Lemma for dochexmid 38606. Contradict dochexmidlem6 38603. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑝 ∈ 𝐴) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑀 = (𝑋 ⊕ 𝑝) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) & ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) ⇒ ⊢ (𝜑 → 𝑀 ≠ 𝑋) | ||
Theorem | dochexmidlem8 38605 | Lemma for dochexmid 38606. The contradiction of dochexmidlem6 38603 and dochexmidlem7 38604 shows that there can be no atom 𝑝 that is not in 𝑋 + ( ⊥ ‘𝑋), which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ { 0 }) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | dochexmid 38606 | Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 38515. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 37116 analog.) (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) ⇒ ⊢ (𝜑 → (𝑋 ⊕ ( ⊥ ‘𝑋)) = 𝑉) | ||
Theorem | dochsnkrlem1 38607 | Lemma for dochsnkr 38610. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) | ||
Theorem | dochsnkrlem2 38608 | Lemma for dochsnkr 38610. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) & ⊢ 𝐴 = (LSAtoms‘𝑈) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴) | ||
Theorem | dochsnkrlem3 38609 | Lemma for dochsnkr 38610. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | dochsnkr 38610 | A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋})) | ||
Theorem | dochsnkr2 38611* | Kernel of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkr 36255. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑋})) | ||
Theorem | dochsnkr2cl 38612* | The 𝑋 determining functional 𝐺 belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) | ||
Theorem | dochflcl 38613* | Closure of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkrcl 36254. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐹) | ||
Theorem | dochfl1 38614* | The value of the explicit functional 𝐺 is 1 at the 𝑋 that determines it. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐷) & ⊢ 1 = (1r‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) | ||
Theorem | dochfln0 38615 | The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑁 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) ≠ 𝑁) | ||
Theorem | dochkr1 38616* | A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 36208. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })(𝐺‘𝑥) = 1 ) | ||
Theorem | dochkr1OLDN 38617* | A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 36208. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 ) | ||
Syntax | clpoN 38618 | Extend class notation with all polarities of a left module or left vector space. |
class LPol | ||
Definition | df-lpolN 38619* | Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.) |
⊢ LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | lpolsetN 38620* | The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑃 = {𝑜 ∈ (𝑆 ↑m 𝒫 𝑉) ∣ ((𝑜‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ((𝑜‘𝑥) ∈ 𝐻 ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}) | ||
Theorem | islpolN 38621* | The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶𝑆 ∧ (( ⊥ ‘𝑉) = { 0 } ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥))))) | ||
Theorem | islpoldN 38622* | Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆) & ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 }) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦)) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘𝑥) ∈ 𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥) ⇒ ⊢ (𝜑 → ⊥ ∈ 𝑃) | ||
Theorem | lpolfN 38623 | Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) ⇒ ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶𝑆) | ||
Theorem | lpolvN 38624 | The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑉) = { 0 }) | ||
Theorem | lpolconN 38625 | Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ⊆ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | lpolsatN 38626 | The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝐻) | ||
Theorem | lpolpolsatN 38627 | Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝑃 = (LPol‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → ⊥ ∈ 𝑃) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑄)) = 𝑄) | ||
Theorem | dochpolN 38628 | The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑃 = (LPol‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ⊥ ∈ 𝑃) | ||
Theorem | lcfl1lem 38629* | Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))) | ||
Theorem | lcfl1 38630* | Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))) | ||
Theorem | lcfl2 38631* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl3 38632* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘(𝐿‘𝐺)) ∈ 𝐴 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl4N 38633* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | lcfl5 38634* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl5a 38635 | Property of a functional with a closed kernel. TODO: Make lcfl5 38634 etc. obsolete and rewrite without 𝐶 hypothesis? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran 𝐼)) | ||
Theorem | lcfl6lem 38636* | Lemma for lcfl6 38638. A functional 𝐺 (whose kernel is closed by dochsnkr 38610) is comletely determined by a vector 𝑋 in the orthocomplement in its kernel at which the functional value is 1. Note that the ∖ { 0 } in the 𝑋 hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ { 0 })) & ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) ⇒ ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))) | ||
Theorem | lcfl7lem 38637* | Lemma for lcfl7N 38639. If two functionals 𝐺 and 𝐽 are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) & ⊢ 𝐽 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑌})𝑣 = (𝑤 + (𝑘 · 𝑌)))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐺 = 𝐽) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | lcfl6 38638* | Property of a functional with a closed kernel. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 36232. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) | ||
Theorem | lcfl7N 38639* | Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that (𝐿‘𝐺) = 𝑉 means the functional is zero by lkr0f 36232. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ((𝐿‘𝐺) = 𝑉 ∨ ∃!𝑥 ∈ (𝑉 ∖ { 0 })𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))))) | ||
Theorem | lcfl8 38640* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8a 38641* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ ∃𝑥 ∈ 𝑉 (𝐿‘𝐺) = ( ⊥ ‘{𝑥}))) | ||
Theorem | lcfl8b 38642* | Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑌 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ (𝐶 ∖ {𝑌})) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝑉 ∖ { 0 })( ⊥ ‘(𝐿‘𝐺)) = (𝑁‘{𝑥})) | ||
Theorem | lcfl9a 38643 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ⊆ (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) | ||
Theorem | lclkrlem1 38644* | The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶) | ||
Theorem | lclkrlem2a 38645 | Lemma for lclkr 38671. Use lshpat 36194 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝐵})) ⇒ ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) | ||
Theorem | lclkrlem2b 38646 | Lemma for lclkr 38671. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) ⇒ ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) | ||
Theorem | lclkrlem2c 38647 | Lemma for lclkr 38671. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐽 = (LSHyp‘𝑈) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽) | ||
Theorem | lclkrlem2d 38648 | Lemma for lclkr 38671. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran 𝐼) | ||
Theorem | lclkrlem2e 38649 | Lemma for lclkr 38671. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐸) = (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2f 38650 | Lemma for lclkr 38671. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺)) & ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽) ⇒ ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2g 38651 | Lemma for lclkr 38671. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺)) & ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2h 38652 | Lemma for lclkr 38671. Eliminate the (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽 hypothesis. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2i 38653 | Lemma for lclkr 38671. Eliminate the (𝐿‘𝐸) ≠ (𝐿‘𝐺) hypothesis. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2j 38654 | Lemma for lclkr 38671. Kernel closure when 𝑌 is zero. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 = 0 ) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2k 38655 | Lemma for lclkr 38671. Kernel closure when 𝑋 is zero. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 = 0 ) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2l 38656 | Lemma for lclkr 38671. Eliminate the 𝑋 ≠ 0, 𝑌 ≠ 0 hypotheses. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐽 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄) & ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2m 38657 | Lemma for lclkr 38671. Construct a vector 𝐵 that makes the sum of functionals zero. Combine with 𝐵 ∈ 𝑉 to shorten overall proof. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝑉 ∧ ((𝐸 + 𝐺)‘𝐵) = 0 )) | ||
Theorem | lclkrlem2n 38658 | Lemma for lclkr 38671. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 ) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2o 38659 | Lemma for lclkr 38671. When 𝐵 is nonzero, the vectors 𝑋 and 𝑌 can't both belong to the hyperplane generated by 𝐵. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) & ⊢ (𝜑 → 𝐵 ≠ (0g‘𝑈)) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵}))) | ||
Theorem | lclkrlem2p 38660 | Lemma for lclkr 38671. When 𝐵 is zero, 𝑋 and 𝑌 must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) & ⊢ (𝜑 → 𝐵 = (0g‘𝑈)) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋})) | ||
Theorem | lclkrlem2q 38661 | Lemma for lclkr 38671. The sum has a closed kernel when 𝐵 is nonzero. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) & ⊢ (𝜑 → 𝐵 ≠ (0g‘𝑈)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2r 38662 | Lemma for lclkr 38671. When 𝐵 is zero, i.e. when 𝑋 and 𝑌 are colinear, the intersection of the kernels of 𝐸 and 𝐺 equal the kernel of 𝐺, so the kernels of 𝐺 and the sum are comparable. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) & ⊢ (𝜑 → 𝐵 = (0g‘𝑈)) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2s 38663 | Lemma for lclkr 38671. Thus, the sum has a closed kernel when 𝐵 is zero. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) & ⊢ (𝜑 → 𝐵 = (0g‘𝑈)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2t 38664 | Lemma for lclkr 38671. We eliminate all hypotheses with 𝐵 here. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2u 38665 | Lemma for lclkr 38671. lclkrlem2t 38664 with 𝑋 and 𝑌 swapped. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ≠ 0 ) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2v 38666 | Lemma for lclkr 38671. When the hypotheses of lclkrlem2u 38665 and lclkrlem2u 38665 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 38606, which requires the orthomodular law dihoml4 38515 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 ) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 ) ⇒ ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = 𝑉) | ||
Theorem | lclkrlem2w 38667 | Lemma for lclkr 38671. This is the same as lclkrlem2u 38665 and lclkrlem2u 38665 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 ) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 ) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2x 38668 | Lemma for lclkr 38671. Eliminate by cases the hypotheses of lclkrlem2u 38665, lclkrlem2u 38665 and lclkrlem2w 38667. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2y 38669 | Lemma for lclkr 38671. Restate the hypotheses for 𝐸 and 𝐺 to say their kernels are closed, in order to eliminate the generating vectors 𝑋 and 𝑌. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐸))) = (𝐿‘𝐸)) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2 38670* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 38645 through lclkrlem2y 38669 are used for the proof. Here we express lclkrlem2y 38669 in terms of membership in the set 𝐶 of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐸 ∈ 𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐶) | ||
Theorem | lclkr 38671* | The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The fM that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝑆) | ||
Theorem | lcfls1lem 38672* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lcfls1N 38673* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))) | ||
Theorem | lcfls1c 38674* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ 𝐷 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐷 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lclkrslem1 38675* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶) | ||
Theorem | lclkrslem2 38676* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. (Contributed by NM, 28-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝐶) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝐸 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐶) | ||
Theorem | lclkrs 38677* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑅 is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr 38671 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 38671 a special case of this? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝑇) | ||
Theorem | lclkrs2 38678* | The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is a subspace of the dual space containing functionals with closed kernels. Note that 𝑅 is the value given by mapdval 38766. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝑅 = {𝑔 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑄)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶)) | ||
Theorem | lcfrvalsnN 38679* | Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑓)) & ⊢ 𝑅 = (𝑁‘{𝐺}) ⇒ ⊢ (𝜑 → 𝑄 = ( ⊥ ‘(𝐿‘𝐺))) | ||
Theorem | lcfrlem1 38680 | Lemma for lcfr 38723. Note that 𝑋 is z in Mario's notes. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) ⇒ ⊢ (𝜑 → (𝐻‘𝑋) = 0 ) | ||
Theorem | lcfrlem2 38681 | Lemma for lcfr 38723. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘𝐻)) | ||
Theorem | lcfrlem3 38682 | Lemma for lcfr 38723. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐿‘𝐻)) | ||
Theorem | lcfrlem4 38683* | Lemma for lcfr 38723. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑉) | ||
Theorem | lcfrlem5 38684* | Lemma for lcfr 38723. The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace 𝑄 is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑓)) & ⊢ (𝜑 → 𝑋 ∈ 𝑄) & ⊢ 𝐶 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝑋) ∈ 𝑄) | ||
Theorem | lcfrlem6 38685* | Lemma for lcfr 38723. Closure of vector sum with colinear vectors. TODO: Move down 𝑁 definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem7 38686* | Lemma for lcfr 38723. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑌 = 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem8 38687* | Lemma for lcf1o 38689 and lcfr 38723. (Contributed by NM, 21-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))) | ||
Theorem | lcfrlem9 38688* | Lemma for lcf1o 38689. (This part has undesirable $d's on 𝐽 and 𝜑 that we remove in lcf1o 38689.) TODO: ugly proof; maybe have better subtheorems or abbreviate some ℩𝑘 expansions with 𝐽‘𝑧? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐽:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄})) | ||
Theorem | lcf1o 38689* | Define a function 𝐽 that provides a bijection from nonzero vectors 𝑉 to nonzero functionals with closed kernels 𝐶. (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐽:(𝑉 ∖ { 0 })–1-1-onto→(𝐶 ∖ {𝑄})) | ||
Theorem | lcfrlem10 38690* | Lemma for lcfr 38723. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹) | ||
Theorem | lcfrlem11 38691* | Lemma for lcfr 38723. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = ( ⊥ ‘{𝑋})) | ||
Theorem | lcfrlem12N 38692* | Lemma for lcfr 38723. (Contributed by NM, 23-Feb-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ 𝐵 = (0g‘𝑆) & ⊢ (𝜑 → 𝑌 ∈ ( ⊥ ‘{𝑋})) ⇒ ⊢ (𝜑 → ((𝐽‘𝑋)‘𝑌) = 𝐵) | ||
Theorem | lcfrlem13 38693* | Lemma for lcfr 38723. (Contributed by NM, 8-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄})) | ||
Theorem | lcfrlem14 38694* | Lemma for lcfr 38723. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ 𝑁 = (LSpan‘𝑈) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) = (𝑁‘{𝑋})) | ||
Theorem | lcfrlem15 38695* | Lemma for lcfr 38723. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋)))) | ||
Theorem | lcfrlem16 38696* | Lemma for lcfr 38723. (Contributed by NM, 8-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝑃 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝐺 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ (𝐸 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐺) | ||
Theorem | lcfrlem17 38697 | Lemma for lcfr 38723. Condition needed more than once. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 })) | ||
Theorem | lcfrlem18 38698 | Lemma for lcfr 38723. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌}))) | ||
Theorem | lcfrlem19 38699 | Lemma for lcfr 38723. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}))) | ||
Theorem | lcfrlem20 38700 | Lemma for lcfr 38723. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |