P. 417 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41601-41700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lcfrlem21 41601	Lemma for lcfr 41623. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
Theorem	lcfrlem22 41602	Lemma for lcfr 41623. (Contributed by NM, 24-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))    &   ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))    &   ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝐴)
Theorem	lcfrlem23 41603	Lemma for lcfr 41623. 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 41604*	Lemma for lcfr 41623. (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 41605*	Lemma for lcfr 41623. Special case of lcfrlem35 41615 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 41606*	Lemma for lcfr 41623. Special case of lcfrlem36 41616 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 41607*	Lemma for lcfr 41623. Special case of lcfrlem37 41617 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 41608*	Lemma for lcfr 41623. 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 41609*	Lemma for lcfr 41623. (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 41610*	Lemma for lcfr 41623. (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 41611*	Lemma for lcfr 41623. (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 41612*	Lemma for lcfr 41623. (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 41613*	Lemma for lcfr 41623. (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 41614*	Lemma for lcfr 41623. (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 41615*	Lemma for lcfr 41623. (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 41616*	Lemma for lcfr 41623. (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 41617*	Lemma for lcfr 41623. (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 41618*	Lemma for lcfr 41623. Combine lcfrlem27 41607 and lcfrlem37 41617. (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 41619*	Lemma for lcfr 41623. 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 41620*	Lemma for lcfr 41623. 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 41621*	Lemma for lcfr 41623. 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 41622*	Lemma for lcfr 41623. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑄 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑄)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐸)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸)
Theorem	lcfr 41623*	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 41624	Extend class notation with vector space of functionals with closed kernels.
class LCDual
Definition	df-lcdual 41625*	Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 41687. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 41663 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 41626*	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 41627*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐷 ↾s {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}))
Theorem	lcdval2 41628*	Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻))    &   ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    ⇒   ⊢ (𝜑 → 𝐶 = (𝐷 ↾s 𝐵))
Theorem	lcdlvec 41629	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 41630	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 41631*	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 41632	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 41633	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 41634	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 41635	Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ + = (+g‘𝐷)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ✚ = (+g‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ✚ = + )
Theorem	lcdvaddval 41636	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 41637	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 41638	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 41639	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 41640	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 41641	Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ · = ( ·𝑠 ‘𝐷)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ ∙ = ( ·𝑠 ‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∙ = · )
Theorem	lcdvsval 41642	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 41643	The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐶)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝑉)
Theorem	lcdlssvscl 41644	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 41645	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 41646	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 41647	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 41648	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 41649	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 41650	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 41651	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 41652	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 41653	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 41654	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 41655	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 41656	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 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹 − 𝐺)‘𝑋) = ((𝐹‘𝑋)𝑆(𝐺‘𝑋)))
Theorem	lcdlss 41657*	Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝐶)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐵 = {𝑓 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆 = (𝑇 ∩ 𝒫 𝐵))
Theorem	lcdlss2N 41658	Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝐶)    &   ⊢ 𝑉 = (Base‘𝐶)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑆 = (𝑇 ∩ 𝒫 𝑉))
Theorem	lcdlsp 41659	Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑀 = (LSpan‘𝐷)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (Base‘𝐶)    &   ⊢ 𝑁 = (LSpan‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐹)    ⇒   ⊢ (𝜑 → (𝑁‘𝐺) = (𝑀‘𝐺))
Theorem	lcdlkreqN 41660	Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 0 = (0g‘𝐶)    &   ⊢ 𝑁 = (LSpan‘𝐶)    &   ⊢ 𝑉 = (Base‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑁‘{𝐼}))    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐼))
Theorem	lcdlkreq2N 41661	Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑈)    &   ⊢ 𝑅 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝐶)    &   ⊢ · = ( ·𝑠 ‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝐴 ∈ (𝑅 ∖ { 0 }))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 = (𝐴 · 𝐼))    ⇒   ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐼))
Syntax	cmpd 41662	Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
class mapd
Definition	df-mapd 41663*	Extend class notation with a one-to-one onto (mapd1o 41686), order-preserving (mapdord 41676) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.)
⊢ mapd = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝑘)‘𝑤)) ∣ ((((ocH‘𝑘)‘𝑤)‘(((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓) ∧ (((ocH‘𝑘)‘𝑤)‘((LKer‘((DVecH‘𝑘)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
Theorem	mapdffval 41664*	Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑋 → (mapd‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑠 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤)) ↦ {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑤)) ∣ ((((ocH‘𝐾)‘𝑤)‘(((ocH‘𝐾)‘𝑤)‘((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓) ∧ (((ocH‘𝐾)‘𝑤)‘((LKer‘((DVecH‘𝐾)‘𝑤))‘𝑓)) ⊆ 𝑠)})))
Theorem	mapdfval 41665*	Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑠 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑠)}))
Theorem	mapdval 41666*	Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇)})
Theorem	mapdvalc 41667*	Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇})
Theorem	mapdval2N 41668*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐶 ∣ ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})})
Theorem	mapdval3N 41669*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = ∪ 𝑣 ∈ 𝑇 {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})})
Theorem	mapdval4N 41670*	Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is ⊆ 𝐶) 2. The unneeded direction of lcfl8a 41541 has awkward ∃- add another thm with only one direction of it? 3. Swap 𝑂‘{𝑣} and 𝐿‘𝑓? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐹 ∣ ∃𝑣 ∈ 𝑇 (𝑂‘{𝑣}) = (𝐿‘𝑓)})
Theorem	mapdval5N 41671*	Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑇) = ∪ 𝑣 ∈ 𝑇 {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑣}) = (𝐿‘𝑓)})
Theorem	mapdordlem1a 41672*	Lemma for mapdord 41676. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑌 = (LSHyp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑇 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) ∈ 𝑌}    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐶 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) ∈ 𝑌)))
Theorem	mapdordlem1bN 41673*	Lemma for mapdord 41676. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)
⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    ⇒   ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ 𝐹 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) = (𝐿‘𝐽)))
Theorem	mapdordlem1 41674*	Lemma for mapdord 41676. (Contributed by NM, 27-Jan-2015.)
⊢ 𝑇 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) ∈ 𝑌}    ⇒   ⊢ (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐹 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) ∈ 𝑌))
Theorem	mapdordlem2 41675*	Lemma for mapdord 41676. Ordering property of projectivity 𝑀. TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the 𝑇 hypothesis. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐽 = (LSHyp‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑇 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) ∈ 𝐽}    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋) ⊆ (𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌))
Theorem	mapdord 41676	Ordering property of the map defined by df-mapd 41663. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋) ⊆ (𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌))
Theorem	mapd11 41677	The map defined by df-mapd 41663 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋) = (𝑀‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	mapddlssN 41678	The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 41694 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑅) ∈ 𝑇)
Theorem	mapdsn 41679*	Value of the map defined by df-mapd 41663 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})
Theorem	mapdsn2 41680*	Value of the map defined by df-mapd 41663 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐿‘𝐺) = (𝑂‘{𝑋}))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑓)})
Theorem	mapdsn3 41681	Value of the map defined by df-mapd 41663 at the span of a singleton. (Contributed by NM, 17-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑃 = (LSpan‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐹)    &   ⊢ (𝜑 → (𝐿‘𝐺) = (𝑂‘{𝑋}))    ⇒   ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝑃‘{𝐺}))
Theorem	mapd1dim2lem1N 41682*	Value of the map defined by df-mapd 41663 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘𝑄) = {𝑓 ∈ 𝐹 ∣ ∃𝑣 ∈ 𝑄 (𝑂‘{𝑣}) = (𝐿‘𝑓)})
Theorem	mapdrvallem2 41683*	Lemma for mapdrval 41685. TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑌 = (0g‘𝐷)    ⇒   ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} ⊆ 𝑅)
Theorem	mapdrvallem3 41684*	Lemma for mapdrval 41685. (Contributed by NM, 2-Feb-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    &   ⊢ 𝑉 = (Base‘𝑈)    &   ⊢ 𝐴 = (LSAtoms‘𝑈)    &   ⊢ 𝑁 = (LSpan‘𝑈)    &   ⊢ 0 = (0g‘𝑈)    &   ⊢ 𝑌 = (0g‘𝐷)    ⇒   ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} = 𝑅)
Theorem	mapdrval 41685*	Given a dual subspace 𝑅 (of functionals with closed kernels), reconstruct the subspace 𝑄 that maps to it. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝐶)    &   ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ))    ⇒   ⊢ (𝜑 → (𝑀‘𝑄) = 𝑅)
Theorem	mapd1o 41686*	The map defined by df-mapd 41663 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows 𝑀 satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 41623, mapdrval 41685, lclkrs 41577, lclkr 41571,...) to use 𝑇 ∩ 𝒫 𝐶? TODO: maybe get rid of $d's for 𝑔 versus 𝐾𝑈𝑊; propagate to mapdrn 41687 and any others. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → 𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶))
Theorem	mapdrn 41687*	Range of the map defined by df-mapd 41663. (Contributed by NM, 12-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐷 = (LDual‘𝑈)    &   ⊢ 𝑇 = (LSubSp‘𝐷)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝑀 = (𝑇 ∩ 𝒫 𝐶))
Theorem	mapdunirnN 41688*	Union of the range of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐹 = (LFnl‘𝑈)    &   ⊢ 𝐿 = (LKer‘𝑈)    &   ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)}    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ∪ ran 𝑀 = 𝐶)
Theorem	mapdrn2 41689	Range of the map defined by df-mapd 41663. TODO: this seems to be needed a lot in hdmaprnlem3eN 41896 etc. Would it be better to change df-mapd 41663 theorems to use LSubSp‘𝐶 instead of ran 𝑀? (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    ⇒   ⊢ (𝜑 → ran 𝑀 = 𝑇)
Theorem	mapdcnvcl 41690	Closure of the converse of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (◡𝑀‘𝑋) ∈ 𝑆)
Theorem	mapdcl 41691	Closure the value of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) ∈ ran 𝑀)
Theorem	mapdcnvid1N 41692	Converse of the value of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (◡𝑀‘(𝑀‘𝑋)) = 𝑋)
Theorem	mapdsord 41693	Strong ordering property of themap defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑋) ⊊ (𝑀‘𝑌) ↔ 𝑋 ⊊ 𝑌))
Theorem	mapdcl2 41694	The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝑇 = (LSubSp‘𝐶)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝑅) ∈ 𝑇)
Theorem	mapdcnvid2 41695	Value of the converse of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (𝑀‘(◡𝑀‘𝑋)) = 𝑋)
Theorem	mapdcnvordN 41696	Ordering property of the converse of the map defined by df-mapd 41663. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → ((◡𝑀‘𝑋) ⊆ (◡𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌))
Theorem	mapdcnv11N 41697	The converse of the map defined by df-mapd 41663 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → ((◡𝑀‘𝑋) = (◡𝑀‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	mapdcv 41698	Covering property of the converse of the map defined by df-mapd 41663. (Contributed by NM, 14-Mar-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ 𝐶 = ( ⋖L ‘𝑈)    &   ⊢ 𝐷 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ( ⋖L ‘𝐷)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑋𝐶𝑌 ↔ (𝑀‘𝑋)𝐸(𝑀‘𝑌)))
Theorem	mapdincl 41699	Closure of dual subspace intersection for the map defined by df-mapd 41663. (Contributed by NM, 12-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝑀)    ⇒   ⊢ (𝜑 → (𝑋 ∩ 𝑌) ∈ ran 𝑀)
Theorem	mapdin 41700	Subspace intersection is preserved by the map defined by df-mapd 41663. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)    &   ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑈)    &   ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝑋 ∩ 𝑌)) = ((𝑀‘𝑋) ∩ (𝑀‘𝑌)))