Metamath Proof Explorer


Theorem hdmap14lem7

Description: Combine cases of F . TODO: Can this be done at once in hdmap14lem3 , in order to get rid of hdmap14lem6 ? Perhaps modify lspsneu to become E! k e. K instead of E! k e. ( K \ { .0. } ) ? (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmap14lem7.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmap14lem7.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem7.v 𝑉 = ( Base ‘ 𝑈 )
hdmap14lem7.t · = ( ·𝑠𝑈 )
hdmap14lem7.o 0 = ( 0g𝑈 )
hdmap14lem7.r 𝑅 = ( Scalar ‘ 𝑈 )
hdmap14lem7.b 𝐵 = ( Base ‘ 𝑅 )
hdmap14lem7.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem7.e = ( ·𝑠𝐶 )
hdmap14lem7.p 𝑃 = ( Scalar ‘ 𝐶 )
hdmap14lem7.a 𝐴 = ( Base ‘ 𝑃 )
hdmap14lem7.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmap14lem7.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem7.f ( 𝜑𝐹𝐵 )
Assertion hdmap14lem7 ( 𝜑 → ∃! 𝑔𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ( 𝑆𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem7.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap14lem7.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap14lem7.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmap14lem7.t · = ( ·𝑠𝑈 )
5 hdmap14lem7.o 0 = ( 0g𝑈 )
6 hdmap14lem7.r 𝑅 = ( Scalar ‘ 𝑈 )
7 hdmap14lem7.b 𝐵 = ( Base ‘ 𝑅 )
8 hdmap14lem7.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 hdmap14lem7.e = ( ·𝑠𝐶 )
10 hdmap14lem7.p 𝑃 = ( Scalar ‘ 𝐶 )
11 hdmap14lem7.a 𝐴 = ( Base ‘ 𝑃 )
12 hdmap14lem7.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
13 hdmap14lem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 hdmap14lem7.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
15 hdmap14lem7.f ( 𝜑𝐹𝐵 )
16 eqid ( 0g𝑅 ) = ( 0g𝑅 )
17 eqid ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
18 eqid ( 0g𝑃 ) = ( 0g𝑃 )
19 13 adantr ( ( 𝜑𝐹 = ( 0g𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
20 14 adantr ( ( 𝜑𝐹 = ( 0g𝑅 ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
21 simpr ( ( 𝜑𝐹 = ( 0g𝑅 ) ) → 𝐹 = ( 0g𝑅 ) )
22 1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 19 20 21 hdmap14lem6 ( ( 𝜑𝐹 = ( 0g𝑅 ) ) → ∃! 𝑔𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ( 𝑆𝑋 ) ) )
23 13 adantr ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
24 14 adantr ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
25 15 adantr ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → 𝐹𝐵 )
26 simpr ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → 𝐹 ≠ ( 0g𝑅 ) )
27 eldifsn ( 𝐹 ∈ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ↔ ( 𝐹𝐵𝐹 ≠ ( 0g𝑅 ) ) )
28 25 26 27 sylanbrc ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → 𝐹 ∈ ( 𝐵 ∖ { ( 0g𝑅 ) } ) )
29 1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 23 24 28 hdmap14lem4 ( ( 𝜑𝐹 ≠ ( 0g𝑅 ) ) → ∃! 𝑔𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ( 𝑆𝑋 ) ) )
30 22 29 pm2.61dane ( 𝜑 → ∃! 𝑔𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ( 𝑆𝑋 ) ) )