Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a into this one. (Contributed by NM, 31-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hdmap14lem1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
hdmap14lem1.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
hdmap14lem1.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | ||
hdmap14lem1.t | ⊢ · = ( ·𝑠 ‘ 𝑈 ) | ||
hdmap14lem3.o | ⊢ 0 = ( 0g ‘ 𝑈 ) | ||
hdmap14lem1.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | ||
hdmap14lem1.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | ||
hdmap14lem1.z | ⊢ 𝑍 = ( 0g ‘ 𝑅 ) | ||
hdmap14lem1.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | ||
hdmap14lem2.e | ⊢ ∙ = ( ·𝑠 ‘ 𝐶 ) | ||
hdmap14lem1.l | ⊢ 𝐿 = ( LSpan ‘ 𝐶 ) | ||
hdmap14lem2.p | ⊢ 𝑃 = ( Scalar ‘ 𝐶 ) | ||
hdmap14lem2.a | ⊢ 𝐴 = ( Base ‘ 𝑃 ) | ||
hdmap14lem2.q | ⊢ 𝑄 = ( 0g ‘ 𝑃 ) | ||
hdmap14lem1.s | ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) | ||
hdmap14lem1.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
hdmap14lem3.x | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ) | ||
hdmap14lem1.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ∖ { 𝑍 } ) ) | ||
Assertion | hdmap14lem4 | ⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmap14lem1.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
2 | hdmap14lem1.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
3 | hdmap14lem1.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | |
4 | hdmap14lem1.t | ⊢ · = ( ·𝑠 ‘ 𝑈 ) | |
5 | hdmap14lem3.o | ⊢ 0 = ( 0g ‘ 𝑈 ) | |
6 | hdmap14lem1.r | ⊢ 𝑅 = ( Scalar ‘ 𝑈 ) | |
7 | hdmap14lem1.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
8 | hdmap14lem1.z | ⊢ 𝑍 = ( 0g ‘ 𝑅 ) | |
9 | hdmap14lem1.c | ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) | |
10 | hdmap14lem2.e | ⊢ ∙ = ( ·𝑠 ‘ 𝐶 ) | |
11 | hdmap14lem1.l | ⊢ 𝐿 = ( LSpan ‘ 𝐶 ) | |
12 | hdmap14lem2.p | ⊢ 𝑃 = ( Scalar ‘ 𝐶 ) | |
13 | hdmap14lem2.a | ⊢ 𝐴 = ( Base ‘ 𝑃 ) | |
14 | hdmap14lem2.q | ⊢ 𝑄 = ( 0g ‘ 𝑃 ) | |
15 | hdmap14lem1.s | ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) | |
16 | hdmap14lem1.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
17 | hdmap14lem3.x | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ) | |
18 | hdmap14lem1.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ∖ { 𝑍 } ) ) | |
19 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 | hdmap14lem3 | ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( 𝐴 ∖ { 𝑄 } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) |
20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 | hdmap14lem4a | ⊢ ( 𝜑 → ( ∃! 𝑔 ∈ ( 𝐴 ∖ { 𝑄 } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) |
21 | 19 20 | mpbid | ⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) |