![]() |
Metamath
Proof Explorer Theorem List (p. 405 of 478) | < 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-30148) |
![]() (30149-31671) |
![]() (31672-47753) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lcdvbase 40401* | 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 40402 | 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 40403 | 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 40404 | 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 40405 | Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ + = (+g‘𝐷) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ✚ = + ) | ||
Theorem | lcdvaddval 40406 | 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 40407 | 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 40408 | 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 40409 | 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 40410 | 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 40411 | Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∙ = · ) | ||
Theorem | lcdvsval 40412 | 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 40413 | The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑈) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝐶) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝑉) | ||
Theorem | lcdlssvscl 40414 | 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 40415 | 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 40416 | 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 40417 | 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 40418 | 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 40419 | 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 40420 | 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 40421 | 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 40422 | 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 40423 | 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 40424 | 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 40425 | 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 40426 | 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 40427* | 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 40428 | 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 40429 | 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 40430 | 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 40431 | 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 40432 | Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels. |
class mapd | ||
Definition | df-mapd 40433* | Extend class notation with a one-to-one onto (mapd1o 40456), order-preserving (mapdord 40446) 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 40434* | 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 40435* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑠 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑠)})) | ||
Theorem | mapdval 40436* | 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 40437* | 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 40438* | 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 40439* | 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 40440* | 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 40311 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 40441* | 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 40442* | Lemma for mapdord 40446. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑇 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) ∈ 𝑌} & ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐶 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) ∈ 𝑌))) | ||
Theorem | mapdordlem1bN 40443* | Lemma for mapdord 40446. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} ⇒ ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ 𝐹 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) = (𝐿‘𝐽))) | ||
Theorem | mapdordlem1 40444* | Lemma for mapdord 40446. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝑇 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) ∈ 𝑌} ⇒ ⊢ (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐹 ∧ (𝑂‘(𝑂‘(𝐿‘𝐽))) ∈ 𝑌)) | ||
Theorem | mapdordlem2 40445* | Lemma for mapdord 40446. 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 40446 | Ordering property of the map defined by df-mapd 40433. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑀‘𝑋) ⊆ (𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌)) | ||
Theorem | mapd11 40447 | The map defined by df-mapd 40433 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑀‘𝑋) = (𝑀‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | mapddlssN 40448 | 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 40464 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝑅) ∈ 𝑇) | ||
Theorem | mapdsn 40449* | Value of the map defined by df-mapd 40433 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)}) | ||
Theorem | mapdsn2 40450* | Value of the map defined by df-mapd 40433 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝐿‘𝐺) = (𝑂‘{𝑋})) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑓)}) | ||
Theorem | mapdsn3 40451 | Value of the map defined by df-mapd 40433 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 40452* | Value of the map defined by df-mapd 40433 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝑄) = {𝑓 ∈ 𝐹 ∣ ∃𝑣 ∈ 𝑄 (𝑂‘{𝑣}) = (𝐿‘𝑓)}) | ||
Theorem | mapdrvallem2 40453* | Lemma for mapdrval 40455. 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 40454* | Lemma for mapdrval 40455. (Contributed by NM, 2-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑅 ∈ 𝑇) & ⊢ (𝜑 → 𝑅 ⊆ 𝐶) & ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 (𝑂‘(𝐿‘ℎ)) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑌 = (0g‘𝐷) ⇒ ⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑄} = 𝑅) | ||
Theorem | mapdrval 40455* | 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 40456* | The map defined by df-mapd 40433 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 40393, mapdrval 40455, lclkrs 40347, lclkr 40341,...) to use 𝑇 ∩ 𝒫 𝐶? TODO: maybe get rid of $d's for 𝑔 versus 𝐾𝑈𝑊; propagate to mapdrn 40457 and any others. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶)) | ||
Theorem | mapdrn 40457* | Range of the map defined by df-mapd 40433. (Contributed by NM, 12-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐷 = (LDual‘𝑈) & ⊢ 𝑇 = (LSubSp‘𝐷) & ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ran 𝑀 = (𝑇 ∩ 𝒫 𝐶)) | ||
Theorem | mapdunirnN 40458* | Union of the range of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ∪ ran 𝑀 = 𝐶) | ||
Theorem | mapdrn2 40459 | Range of the map defined by df-mapd 40433. TODO: this seems to be needed a lot in hdmaprnlem3eN 40666 etc. Would it be better to change df-mapd 40433 theorems to use LSubSp‘𝐶 instead of ran 𝑀? (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝑇 = (LSubSp‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ran 𝑀 = 𝑇) | ||
Theorem | mapdcnvcl 40460 | Closure of the converse of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → (◡𝑀‘𝑋) ∈ 𝑆) | ||
Theorem | mapdcl 40461 | Closure the value of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝑋) ∈ ran 𝑀) | ||
Theorem | mapdcnvid1N 40462 | Converse of the value of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → (◡𝑀‘(𝑀‘𝑋)) = 𝑋) | ||
Theorem | mapdsord 40463 | Strong ordering property of themap defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑀‘𝑋) ⊊ (𝑀‘𝑌) ↔ 𝑋 ⊊ 𝑌)) | ||
Theorem | mapdcl2 40464 | 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 40465 | Value of the converse of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → (𝑀‘(◡𝑀‘𝑋)) = 𝑋) | ||
Theorem | mapdcnvordN 40466 | Ordering property of the converse of the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) & ⊢ (𝜑 → 𝑌 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → ((◡𝑀‘𝑋) ⊆ (◡𝑀‘𝑌) ↔ 𝑋 ⊆ 𝑌)) | ||
Theorem | mapdcnv11N 40467 | The converse of the map defined by df-mapd 40433 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) & ⊢ (𝜑 → 𝑌 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → ((◡𝑀‘𝑋) = (◡𝑀‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | mapdcv 40468 | Covering property of the converse of the map defined by df-mapd 40433. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐶 = ( ⋖L ‘𝑈) & ⊢ 𝐷 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐸 = ( ⋖L ‘𝐷) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐶𝑌 ↔ (𝑀‘𝑋)𝐸(𝑀‘𝑌))) | ||
Theorem | mapdincl 40469 | Closure of dual subspace intersection for the map defined by df-mapd 40433. (Contributed by NM, 12-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) & ⊢ (𝜑 → 𝑌 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → (𝑋 ∩ 𝑌) ∈ ran 𝑀) | ||
Theorem | mapdin 40470 | Subspace intersection is preserved by the map defined by df-mapd 40433. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘(𝑋 ∩ 𝑌)) = ((𝑀‘𝑋) ∩ (𝑀‘𝑌))) | ||
Theorem | mapdlsmcl 40471 | Closure of dual subspace sum for the map defined by df-mapd 40433. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑀) & ⊢ (𝜑 → 𝑌 ∈ ran 𝑀) ⇒ ⊢ (𝜑 → (𝑋 ⊕ 𝑌) ∈ ran 𝑀) | ||
Theorem | mapdlsm 40472 | Subspace sum is preserved by the map defined by df-mapd 40433. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ ✚ = (LSSum‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘(𝑋 ⊕ 𝑌)) = ((𝑀‘𝑋) ✚ (𝑀‘𝑌))) | ||
Theorem | mapd0 40473 | Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑂 = (0g‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝑀‘{𝑂}) = { 0 }) | ||
Theorem | mapdcnvatN 40474 | Atoms are preserved by the map defined by df-mapd 40433. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐵 = (LSAtoms‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) ⇒ ⊢ (𝜑 → (◡𝑀‘𝑄) ∈ 𝐴) | ||
Theorem | mapdat 40475 | Atoms are preserved by the map defined by df-mapd 40433. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐵 = (LSAtoms‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘𝑄) ∈ 𝐵) | ||
Theorem | mapdspex 40476* | The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝐵 (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝑔})) | ||
Theorem | mapdn0 40477 | Transfer nonzero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑍 = (0g‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐷 ∖ {𝑍})) | ||
Theorem | mapdncol 40478 | Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺})) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝐽‘{𝐹}) ≠ (𝐽‘{𝐺})) | ||
Theorem | mapdindp 40479 | Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ 𝐷 = (Base‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺})) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝐷) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸})) | ||
Theorem | mapdpglem1 40480 | Lemma for mapdpg 40514. Baer p. 44, last line: "(F(x-y))* <= (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) ⊆ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) | ||
Theorem | mapdpglem2 40481* | Lemma for mapdpg 40514. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d 𝑡𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 15-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))(𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) | ||
Theorem | mapdpglem2a 40482* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) ⇒ ⊢ (𝜑 → 𝑡 ∈ 𝐹) | ||
Theorem | mapdpglem3 40483* | Lemma for mapdpg 40514. Baer p. 45, line 3: "infer ... the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d 𝑔𝑤𝑧𝜑 locally to avoid clashes with later substitutions into 𝜑.) (Contributed by NM, 18-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝐵 ∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) | ||
Theorem | mapdpglem4N 40484* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 𝑄) | ||
Theorem | mapdpglem5N 40485* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ⇒ ⊢ (𝜑 → 𝑡 ≠ (0g‘𝐶)) | ||
Theorem | mapdpglem6 40486* | Lemma for mapdpg 40514. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑔 = 0 ) ⇒ ⊢ (𝜑 → 𝑡 ∈ (𝑀‘(𝑁‘{𝑌}))) | ||
Theorem | mapdpglem8 40487* | Lemma for mapdpg 40514. Baer p. 45, line 4: "...so that (F(x-y))* <= (Fy)*. This would imply that F(x-y) <= F(y)..." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑔 = 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ⊆ (𝑁‘{𝑌})) | ||
Theorem | mapdpglem9 40488* | Lemma for mapdpg 40514. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑔 = 0 ) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌})) | ||
Theorem | mapdpglem10 40489* | Lemma for mapdpg 40514. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑔 = 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) | ||
Theorem | mapdpglem11 40490* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝑔 ≠ 0 ) | ||
Theorem | mapdpglem12 40491* | Lemma for mapdpg 40514. TODO: Can some commonality with mapdpglem6 40486 through mapdpglem11 40490 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ (𝜑 → 𝑧 = (0g‘𝐶)) ⇒ ⊢ (𝜑 → 𝑡 ∈ (𝑀‘(𝑁‘{𝑋}))) | ||
Theorem | mapdpglem13 40492* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ (𝜑 → 𝑧 = (0g‘𝐶)) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) ⊆ (𝑁‘{𝑋})) | ||
Theorem | mapdpglem14 40493* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ (𝜑 → 𝑧 = (0g‘𝐶)) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) | ||
Theorem | mapdpglem15 40494* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ (𝜑 → 𝑧 = (0g‘𝐶)) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) | ||
Theorem | mapdpglem16 40495* | Lemma for mapdpg 40514. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) ⇒ ⊢ (𝜑 → 𝑧 ≠ (0g‘𝐶)) | ||
Theorem | mapdpglem17N 40496* | Lemma for mapdpg 40514. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝐹) | ||
Theorem | mapdpglem18 40497* | Lemma for mapdpg 40514. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧) ⇒ ⊢ (𝜑 → 𝐸 ≠ (0g‘𝐶)) | ||
Theorem | mapdpglem19 40498* | Lemma for mapdpg 40514. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝑀‘(𝑁‘{𝑌}))) | ||
Theorem | mapdpglem20 40499* | Lemma for mapdpg 40514. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧) ⇒ ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐸})) | ||
Theorem | mapdpglem21 40500* | Lemma for mapdpg 40514. (Contributed by NM, 20-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ⊕ = (LSSum‘𝐶) & ⊢ 𝐽 = (LSpan‘𝐶) & ⊢ 𝐹 = (Base‘𝐶) & ⊢ (𝜑 → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋})) ⊕ (𝑀‘(𝑁‘{𝑌})))) & ⊢ 𝐴 = (Scalar‘𝑈) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑅 = (-g‘𝐶) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) & ⊢ 𝑄 = (0g‘𝑈) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) & ⊢ 0 = (0g‘𝐴) & ⊢ (𝜑 → 𝑔 ∈ 𝐵) & ⊢ (𝜑 → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) & ⊢ (𝜑 → 𝑡 = ((𝑔 · 𝐺)𝑅𝑧)) & ⊢ (𝜑 → 𝑋 ≠ 𝑄) & ⊢ (𝜑 → 𝑌 ≠ 𝑄) & ⊢ 𝐸 = (((invr‘𝐴)‘𝑔) · 𝑧) ⇒ ⊢ (𝜑 → (((invr‘𝐴)‘𝑔) · 𝑡) = (𝐺𝑅𝐸)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |