Metamath Proof Explorer


Theorem hdmap14lem8

Description: Part of proof of part 14 in Baer p. 49 lines 33-35. (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 hdmap14lem8 ( 𝜑 → ( ( 𝐽 ( 𝑆𝑋 ) ) ( 𝐽 ( 𝑆𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )

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 1 10 16 lcdlmod ( 𝜑𝐶 ∈ LMod )
28 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
29 17 eldifad ( 𝜑𝑋𝑉 )
30 1 2 3 10 28 15 16 29 hdmapcl ( 𝜑 → ( 𝑆𝑋 ) ∈ ( Base ‘ 𝐶 ) )
31 18 eldifad ( 𝜑𝑌𝑉 )
32 1 2 3 10 28 15 16 31 hdmapcl ( 𝜑 → ( 𝑆𝑌 ) ∈ ( Base ‘ 𝐶 ) )
33 28 11 13 12 14 lmodvsdi ( ( 𝐶 ∈ LMod ∧ ( 𝐽𝐴 ∧ ( 𝑆𝑋 ) ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑆𝑌 ) ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐽 ( ( 𝑆𝑋 ) ( 𝑆𝑌 ) ) ) = ( ( 𝐽 ( 𝑆𝑋 ) ) ( 𝐽 ( 𝑆𝑌 ) ) ) )
34 27 25 30 32 33 syl13anc ( 𝜑 → ( 𝐽 ( ( 𝑆𝑋 ) ( 𝑆𝑌 ) ) ) = ( ( 𝐽 ( 𝑆𝑋 ) ) ( 𝐽 ( 𝑆𝑌 ) ) ) )
35 1 2 3 4 10 11 15 16 29 31 hdmapadd ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆𝑋 ) ( 𝑆𝑌 ) ) )
36 35 oveq2d ( 𝜑 → ( 𝐽 ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝐽 ( ( 𝑆𝑋 ) ( 𝑆𝑌 ) ) ) )
37 1 2 16 dvhlmod ( 𝜑𝑈 ∈ LMod )
38 3 4 8 5 9 lmodvsdi ( ( 𝑈 ∈ LMod ∧ ( 𝐹𝐵𝑋𝑉𝑌𝑉 ) ) → ( 𝐹 · ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 · 𝑋 ) + ( 𝐹 · 𝑌 ) ) )
39 37 19 29 31 38 syl13anc ( 𝜑 → ( 𝐹 · ( 𝑋 + 𝑌 ) ) = ( ( 𝐹 · 𝑋 ) + ( 𝐹 · 𝑌 ) ) )
40 39 fveq2d ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · ( 𝑋 + 𝑌 ) ) ) = ( 𝑆 ‘ ( ( 𝐹 · 𝑋 ) + ( 𝐹 · 𝑌 ) ) ) )
41 3 8 5 9 lmodvscl ( ( 𝑈 ∈ LMod ∧ 𝐹𝐵𝑋𝑉 ) → ( 𝐹 · 𝑋 ) ∈ 𝑉 )
42 37 19 29 41 syl3anc ( 𝜑 → ( 𝐹 · 𝑋 ) ∈ 𝑉 )
43 3 8 5 9 lmodvscl ( ( 𝑈 ∈ LMod ∧ 𝐹𝐵𝑌𝑉 ) → ( 𝐹 · 𝑌 ) ∈ 𝑉 )
44 37 19 31 43 syl3anc ( 𝜑 → ( 𝐹 · 𝑌 ) ∈ 𝑉 )
45 1 2 3 4 10 11 15 16 42 44 hdmapadd ( 𝜑 → ( 𝑆 ‘ ( ( 𝐹 · 𝑋 ) + ( 𝐹 · 𝑌 ) ) ) = ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) ) )
46 22 23 oveq12d ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )
47 40 45 46 3eqtrd ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · ( 𝑋 + 𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )
48 26 47 eqtr3d ( 𝜑 → ( 𝐽 ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )
49 36 48 eqtr3d ( 𝜑 → ( 𝐽 ( ( 𝑆𝑋 ) ( 𝑆𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )
50 34 49 eqtr3d ( 𝜑 → ( ( 𝐽 ( 𝑆𝑋 ) ) ( 𝐽 ( 𝑆𝑌 ) ) ) = ( ( 𝐺 ( 𝑆𝑋 ) ) ( 𝐼 ( 𝑆𝑌 ) ) ) )