Metamath Proof Explorer

Theorem mapdpglem27

Description: Lemma for mapdpg . Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
mapdpgem25.h1 ⊢ ( 𝜑 → ( ℎ ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
mapdpgem25.i1 ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ) ) )
mapdpglem26.a ⊢ 𝐴 = ( Scalar ‘ 𝑈 )
mapdpglem26.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mapdpglem26.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
mapdpglem26.o ⊢ 𝑂 = ( 0g ‘ 𝐴 )
Assertion mapdpglem27 ( 𝜑 → ∃ 𝑣 ∈ ( 𝐵 ∖ { 𝑂 } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
6 mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
10 mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
11 mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
12 mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14 mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
15 mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
16 mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17 mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
18 mapdpgem25.h1 ⊢ ( 𝜑 → ( ℎ ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
19 mapdpgem25.i1 ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ) ) )
20 mapdpglem26.a ⊢ 𝐴 = ( Scalar ‘ 𝑈 )
21 mapdpglem26.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
22 mapdpglem26.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
23 mapdpglem26.o ⊢ 𝑂 = ( 0g ‘ 𝐴 )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdpglem25 ⊢ ( 𝜑 → ( ( 𝐽 ‘ { ℎ } ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ) )
25 24 simprd ⊢ ( 𝜑 → ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) )
26 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
28 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) )
29 1 8 12 lcdlvec ⊢ ( 𝜑 → 𝐶 ∈ LVec )
30 1 8 12 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
31 18 simpld ⊢ ( 𝜑 → ℎ ∈ 𝐹 )
32 9 10 lmodvsubcl ⊢ ( ( 𝐶 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ℎ ∈ 𝐹 ) → ( 𝐺 𝑅 ℎ ) ∈ 𝐹 )
33 30 15 31 32 syl3anc ⊢ ( 𝜑 → ( 𝐺 𝑅 ℎ ) ∈ 𝐹 )
34 19 simpld ⊢ ( 𝜑 → 𝑖 ∈ 𝐹 )
35 9 10 lmodvsubcl ⊢ ( ( 𝐶 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑖 ∈ 𝐹 ) → ( 𝐺 𝑅 𝑖 ) ∈ 𝐹 )
36 30 15 34 35 syl3anc ⊢ ( 𝜑 → ( 𝐺 𝑅 𝑖 ) ∈ 𝐹 )
37 9 26 27 28 22 11 29 33 36 lspsneq ⊢ ( 𝜑 → ( ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) ) )
38 1 3 20 21 8 26 27 12 lcdsbase ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝐵 )
39 1 3 20 23 8 26 28 12 lcd0 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = 𝑂 )
40 39 sneqd ⊢ ( 𝜑 → { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } = { 𝑂 } )
41 38 40 difeq12d ⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) = ( 𝐵 ∖ { 𝑂 } ) )
42 41 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) ↔ ∃ 𝑣 ∈ ( 𝐵 ∖ { 𝑂 } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) ) )
43 37 42 bitrd ⊢ ( 𝜑 → ( ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ↔ ∃ 𝑣 ∈ ( 𝐵 ∖ { 𝑂 } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) ) )
44 25 43 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝐵 ∖ { 𝑂 } ) ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) )