Metamath Proof Explorer


Theorem hdmap14lem9

Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmap14lem8.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmap14lem8.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.v 𝑉 = ( Base ‘ 𝑈 )
hdmap14lem8.q + = ( +g𝑈 )
hdmap14lem8.t · = ( ·𝑠𝑈 )
hdmap14lem8.o 0 = ( 0g𝑈 )
hdmap14lem8.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmap14lem8.r 𝑅 = ( Scalar ‘ 𝑈 )
hdmap14lem8.b 𝐵 = ( Base ‘ 𝑅 )
hdmap14lem8.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.d = ( +g𝐶 )
hdmap14lem8.e = ( ·𝑠𝐶 )
hdmap14lem8.p 𝑃 = ( Scalar ‘ 𝐶 )
hdmap14lem8.a 𝐴 = ( Base ‘ 𝑃 )
hdmap14lem8.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmap14lem8.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem8.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem8.f ( 𝜑𝐹𝐵 )
hdmap14lem8.g ( 𝜑𝐺𝐴 )
hdmap14lem8.i ( 𝜑𝐼𝐴 )
hdmap14lem8.xx ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ( 𝑆𝑋 ) ) )
hdmap14lem8.yy ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) = ( 𝐼 ( 𝑆𝑌 ) ) )
hdmap14lem8.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
hdmap14lem8.j ( 𝜑𝐽𝐴 )
hdmap14lem8.xy ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · ( 𝑋 + 𝑌 ) ) ) = ( 𝐽 ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) ) )
Assertion hdmap14lem9 ( 𝜑𝐺 = 𝐼 )

Proof

Step Hyp Ref Expression
1 hdmap14lem8.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap14lem8.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap14lem8.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmap14lem8.q + = ( +g𝑈 )
5 hdmap14lem8.t · = ( ·𝑠𝑈 )
6 hdmap14lem8.o 0 = ( 0g𝑈 )
7 hdmap14lem8.n 𝑁 = ( LSpan ‘ 𝑈 )
8 hdmap14lem8.r 𝑅 = ( Scalar ‘ 𝑈 )
9 hdmap14lem8.b 𝐵 = ( Base ‘ 𝑅 )
10 hdmap14lem8.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
11 hdmap14lem8.d = ( +g𝐶 )
12 hdmap14lem8.e = ( ·𝑠𝐶 )
13 hdmap14lem8.p 𝑃 = ( Scalar ‘ 𝐶 )
14 hdmap14lem8.a 𝐴 = ( Base ‘ 𝑃 )
15 hdmap14lem8.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
16 hdmap14lem8.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
17 hdmap14lem8.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 hdmap14lem8.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
19 hdmap14lem8.f ( 𝜑𝐹𝐵 )
20 hdmap14lem8.g ( 𝜑𝐺𝐴 )
21 hdmap14lem8.i ( 𝜑𝐼𝐴 )
22 hdmap14lem8.xx ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ( 𝑆𝑋 ) ) )
23 hdmap14lem8.yy ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) = ( 𝐼 ( 𝑆𝑌 ) ) )
24 hdmap14lem8.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
25 hdmap14lem8.j ( 𝜑𝐽𝐴 )
26 hdmap14lem8.xy ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · ( 𝑋 + 𝑌 ) ) ) = ( 𝐽 ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) ) )
27 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
28 eqid ( 0g𝐶 ) = ( 0g𝐶 )
29 eqid ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
30 1 10 16 lcdlvec ( 𝜑𝐶 ∈ LVec )
31 1 2 3 6 10 28 27 15 16 17 hdmapnzcl ( 𝜑 → ( 𝑆𝑋 ) ∈ ( ( Base ‘ 𝐶 ) ∖ { ( 0g𝐶 ) } ) )
32 1 2 3 6 10 28 27 15 16 18 hdmapnzcl ( 𝜑 → ( 𝑆𝑌 ) ∈ ( ( Base ‘ 𝐶 ) ∖ { ( 0g𝐶 ) } ) )
33 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
34 eqid ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
35 1 2 16 dvhlmod ( 𝜑𝑈 ∈ LMod )
36 17 eldifad ( 𝜑𝑋𝑉 )
37 3 33 7 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 35 36 37 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 18 eldifad ( 𝜑𝑌𝑉 )
40 3 33 7 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑌𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
41 35 39 40 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
42 1 2 33 34 16 38 41 mapd11 ( 𝜑 → ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
43 42 necon3bid ( 𝜑 → ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
44 24 43 mpbird ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑌 } ) ) )
45 1 2 3 7 10 29 34 15 16 36 hdmap10 ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆𝑋 ) } ) )
46 1 2 3 7 10 29 34 15 16 39 hdmap10 ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆𝑌 ) } ) )
47 44 45 46 3netr3d ( 𝜑 → ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆𝑋 ) } ) ≠ ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆𝑌 ) } ) )
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 hdmap14lem8 ( 𝜑 → ( ( 𝐽 ( 𝑆𝑋 ) ) ( 𝐽 ( 𝑆𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )
49 27 11 13 14 12 28 29 30 31 32 25 25 20 21 47 48 lvecindp2 ( 𝜑 → ( 𝐽 = 𝐺𝐽 = 𝐼 ) )
50 49 simpld ( 𝜑𝐽 = 𝐺 )
51 49 simprd ( 𝜑𝐽 = 𝐼 )
52 50 51 eqtr3d ( 𝜑𝐺 = 𝐼 )