![]() |
Metamath
Proof Explorer Theorem List (p. 416 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lclkrlem2m 41501 | Lemma for lclkr 41515. 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 41502 | Lemma for lclkr 41515. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ − = (-g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) = 0 ) & ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) = 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2o 41503 | Lemma for lclkr 41515. 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 41504 | Lemma for lclkr 41515. 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 41505 | Lemma for lclkr 41515. 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 41506 | Lemma for lclkr 41515. 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 41507 | Lemma for lclkr 41515. 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 41508 | Lemma for lclkr 41515. 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 41509 | Lemma for lclkr 41515. lclkrlem2t 41508 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 41510 | Lemma for lclkr 41515. When the hypotheses of lclkrlem2u 41509 and lclkrlem2u 41509 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 41450, which requires the orthomodular law dihoml4 41359 (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 41511 | Lemma for lclkr 41515. This is the same as lclkrlem2u 41509 and lclkrlem2u 41509 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 41512 | Lemma for lclkr 41515. Eliminate by cases the hypotheses of lclkrlem2u 41509, lclkrlem2u 41509 and lclkrlem2w 41511. (Contributed by NM, 18-Jan-2015.) |
⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋})) & ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))) | ||
Theorem | lclkrlem2y 41513 | Lemma for lclkr 41515. 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 41514* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 41489 through lclkrlem2y 41513 are used for the proof. Here we express lclkrlem2y 41513 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 41515* | 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 41516* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lcfls1N 41517* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝐶 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄))) | ||
Theorem | lcfls1c 41518* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} & ⊢ 𝐷 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐷 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) | ||
Theorem | lclkrslem1 41519* | 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 41520* | 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 41521* | 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 41515 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 41515 a special case of this? (Contributed by NM, 29-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝑇) | ||
Theorem | lclkrs2 41522* | 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 41610. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝑅 = {𝑔 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥ ‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑄)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶)) | ||
Theorem | lcfrvalsnN 41523* | 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 41524 | Lemma for lcfr 41567. 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 41525 | Lemma for lcfr 41567. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘𝐻)) | ||
Theorem | lcfrlem3 41526 | Lemma for lcfr 41567. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ × = (.r‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐼 = (invr‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑈 ∈ LVec) & ⊢ (𝜑 → 𝐸 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) & ⊢ 𝐻 = (𝐸 − (((𝐼‘(𝐺‘𝑋)) × (𝐸‘𝑋)) · 𝐺)) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐿‘𝐻)) | ||
Theorem | lcfrlem4 41527* | Lemma for lcfr 41567. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑉) | ||
Theorem | lcfrlem5 41528* | Lemma for lcfr 41567. 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 41529* | Lemma for lcfr 41567. 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 41530* | Lemma for lcfr 41567. 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 41531* | Lemma for lcf1o 41533 and lcfr 41567. (Contributed by NM, 21-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))) | ||
Theorem | lcfrlem9 41532* | Lemma for lcf1o 41533. (This part has undesirable $d's on 𝐽 and 𝜑 that we remove in lcf1o 41533.) 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 41533* | 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 41534* | Lemma for lcfr 41567. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹) | ||
Theorem | lcfrlem11 41535* | Lemma for lcfr 41567. (Contributed by NM, 23-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = ( ⊥ ‘{𝑋})) | ||
Theorem | lcfrlem12N 41536* | Lemma for lcfr 41567. (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 41537* | Lemma for lcfr 41567. (Contributed by NM, 8-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄})) | ||
Theorem | lcfrlem14 41538* | Lemma for lcfr 41567. (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 41539* | Lemma for lcfr 41567. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (0g‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋)))) | ||
Theorem | lcfrlem16 41540* | Lemma for lcfr 41567. (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 41541 | Lemma for lcfr 41567. 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 41542 | Lemma for lcfr 41567. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌}))) | ||
Theorem | lcfrlem19 41543 | Lemma for lcfr 41567. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}))) | ||
Theorem | lcfrlem20 41544 | Lemma for lcfr 41567. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴) | ||
Theorem | lcfrlem21 41545 | Lemma for lcfr 41567. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴) | ||
Theorem | lcfrlem22 41546 | Lemma for lcfr 41567. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐴) | ||
Theorem | lcfrlem23 41547 | Lemma for lcfr 41567. TODO: this proof was built from other proof pieces that may change 𝑁‘{𝑋, 𝑌} into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ ⊕ = (LSSum‘𝑈) ⇒ ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌}) ⊕ 𝐵) = ( ⊥ ‘{(𝑋 + 𝑌)})) | ||
Theorem | lcfrlem24 41548* | Lemma for lcfr 41567. (Contributed by NM, 24-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) ⇒ ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌)))) | ||
Theorem | lcfrlem25 41549* | Lemma for lcfr 41567. Special case of lcfrlem35 41559 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) & ⊢ (𝜑 → 𝐼 ≠ 0 ) ⇒ ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘(𝐽‘𝑌))) | ||
Theorem | lcfrlem26 41550* | Lemma for lcfr 41567. Special case of lcfrlem36 41560 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) & ⊢ (𝜑 → 𝐼 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) | ||
Theorem | lcfrlem27 41551* | Lemma for lcfr 41567. Special case of lcfrlem37 41561 when ((𝐽‘𝑌)‘𝐼) is zero. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) & ⊢ (𝜑 → 𝐼 ≠ 0 ) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝐷)) & ⊢ (𝜑 → 𝐺 ⊆ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem28 41552* | Lemma for lcfr 41567. TODO: This can be a hypothesis since the zero version of (𝐽‘𝑌)‘𝐼 needs it. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝐼 ≠ 0 ) | ||
Theorem | lcfrlem29 41553* | Lemma for lcfr 41567. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) ⇒ ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅) | ||
Theorem | lcfrlem30 41554* | Lemma for lcfr 41567. (Contributed by NM, 6-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) ⇒ ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈)) | ||
Theorem | lcfrlem31 41555* | Lemma for lcfr 41567. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) & ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄) & ⊢ (𝜑 → 𝐶 = (0g‘𝐷)) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) | ||
Theorem | lcfrlem32 41556* | Lemma for lcfr 41567. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) & ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷)) | ||
Theorem | lcfrlem33 41557* | Lemma for lcfr 41567. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) & ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) = 𝑄) ⇒ ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷)) | ||
Theorem | lcfrlem34 41558* | Lemma for lcfr 41567. (Contributed by NM, 10-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) ⇒ ⊢ (𝜑 → 𝐶 ≠ (0g‘𝐷)) | ||
Theorem | lcfrlem35 41559* | Lemma for lcfr 41567. (Contributed by NM, 2-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) ⇒ ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)) | ||
Theorem | lcfrlem36 41560* | Lemma for lcfr 41567. (Contributed by NM, 6-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ ( ⊥ ‘(𝐿‘𝐶))) | ||
Theorem | lcfrlem37 41561* | Lemma for lcfr 41567. (Contributed by NM, 8-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑄 = (0g‘𝑆) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) & ⊢ 𝐹 = (invr‘𝑆) & ⊢ − = (-g‘𝐷) & ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠 ‘𝐷)(𝐽‘𝑌))) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝐷)) & ⊢ (𝜑 → 𝐺 ⊆ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem38 41562* | Lemma for lcfr 41567. Combine lcfrlem27 41551 and lcfrlem37 41561. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ≠ 0 ) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem39 41563* | Lemma for lcfr 41567. Eliminate 𝐽. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) & ⊢ (𝜑 → 𝐼 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem40 41564* | Lemma for lcfr 41567. Eliminate 𝐵 and 𝐼. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem41 41565* | Lemma for lcfr 41567. Eliminate span condition. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfrlem42 41566* | Lemma for lcfr 41567. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑄 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑄) & ⊢ (𝜑 → 𝐺 ⊆ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐸) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) | ||
Theorem | lcfr 41567* | Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑇) & ⊢ (𝜑 → 𝑅 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝑆) | ||
Syntax | clcd 41568 | Extend class notation with vector space of functionals with closed kernels. |
class LCDual | ||
Definition | df-lcdual 41569* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 41631. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 41607 using (Base‘((LCDual‘𝐾)‘𝑊)). (Contributed by NM, 13-Mar-2015.) |
⊢ LCDual = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((LDual‘((DVecH‘𝑘)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ (((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)}))) | ||
Theorem | lcdfval 41570* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑋 → (LCDual‘𝐾) = (𝑤 ∈ 𝐻 ↦ ((LDual‘((DVecH‘𝐾)‘𝑤)) ↾s {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑤)) ∣ (((ocH‘𝐾)‘𝑤)‘(((ocH‘𝐾)‘𝑤)‘((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓)}))) | ||
Theorem | lcdval 41571* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↾s {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)})) | ||
Theorem | lcdval2 41572* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻)) & ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↾s 𝐵)) | ||
Theorem | lcdlvec 41573 | The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 ∈ LVec) | ||
Theorem | lcdlmod 41574 | The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐶 ∈ LMod) | ||
Theorem | lcdvbase 41575* | Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑉 = 𝐵) | ||
Theorem | lcdvbasess 41576 | The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑉 ⊆ 𝐹) | ||
Theorem | lcdvbaselfl 41577 | A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐹) | ||
Theorem | lcdvbasecl 41578 | Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐸 = (Base‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐸) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝑅) | ||
Theorem | lcdvadd 41579 | Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ✚ = + ) | ||
Theorem | lcdvaddval 41580 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ + = (+g‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ ✚ = (+g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐹 ✚ 𝐺)‘𝑋) = ((𝐹‘𝑋) + (𝐺‘𝑋))) | ||
Theorem | lcdsca 41581 | The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑂 = (oppr‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑅 = 𝑂) | ||
Theorem | lcdsbase 41582 | Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐿 = (Base‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑅 = 𝐿) | ||
Theorem | lcdsadd 41583 | Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ + = (+g‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ ✚ = (+g‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ✚ = + ) | ||
Theorem | lcdsmul 41584 | Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐿 = (Base‘𝐹) & ⊢ · = (.r‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ ∙ = (.r‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐿) & ⊢ (𝜑 → 𝑌 ∈ 𝐿) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝑌) = (𝑌 · 𝑋)) | ||
Theorem | lcdvs 41585 | Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∙ = · ) | ||
Theorem | lcdvsval 41586 | Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐺)‘𝐴) = ((𝐺‘𝐴) · 𝑋)) | ||
Theorem | lcdvscl 41587 | The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝑉) | ||
Theorem | lcdlssvscl 41588 | Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑆 = (LSubSp‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐿 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝑌 ∈ 𝐿) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐿) | ||
Theorem | lcdvsass 41589 | Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝐿 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝐿) & ⊢ (𝜑 → 𝑌 ∈ 𝐿) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑌 · 𝑋) ∙ 𝐺) = (𝑋 ∙ (𝑌 ∙ 𝐺))) | ||
Theorem | lcd0 41590 | The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ 𝑂 = (0g‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑂 = 0 ) | ||
Theorem | lcd1 41591 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 1 = (1r‘𝐹) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ 𝐼 = (1r‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐼 = 1 ) | ||
Theorem | lcdneg 41592 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑀 = (invg‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐶) & ⊢ 𝑁 = (invg‘𝑆) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑁 = 𝑀) | ||
Theorem | lcd0v 41593 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑂 = (𝑉 × { 0 })) | ||
Theorem | lcd0v2 41594 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑂 = 0 ) | ||
Theorem | lcd0vvalN 41595 | Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑂‘𝑋) = 0 ) | ||
Theorem | lcd0vcl 41596 | Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑂 ∈ 𝑉) | ||
Theorem | lcd0vs 41597 | A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑂 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( 0 · 𝐺) = 𝑂) | ||
Theorem | lcdvs0N 41598 | A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 0 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) ⇒ ⊢ (𝜑 → (𝑋 · 0 ) = 0 ) | ||
Theorem | lcdvsub 41599 | The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑁 = (invg‘𝑆) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ + = (+g‘𝐶) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ − = (-g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 − 𝐺) = (𝐹 + ((𝑁‘ 1 ) · 𝐺))) | ||
Theorem | lcdvsubval 41600 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑅 = (Scalar‘𝑈) & ⊢ 𝑆 = (-g‘𝑅) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ − = (-g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐹 − 𝐺)‘𝑋) = ((𝐹‘𝑋)𝑆(𝐺‘𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |