Theorem mapdpglem26

Description: Lemma for mapdpg . Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d u ph locally to avoid clashes with later substitutions into ph .) (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	mapdpglem26	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝐵 ∖ { 𝑂 } ) ℎ = ( 𝑢 · 𝑖 ) )

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	simpld	⊢ ( 𝜑 → ( 𝐽 ‘ { ℎ } ) = ( 𝐽 ‘ { 𝑖 } ) )
26		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
27		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
28		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) )
29	1 8 12	lcdlvec	⊢ ( 𝜑 → 𝐶 ∈ LVec )
30	18	simpld	⊢ ( 𝜑 → ℎ ∈ 𝐹 )
31	19	simpld	⊢ ( 𝜑 → 𝑖 ∈ 𝐹 )
32	9 26 27 28 22 11 29 30 31	lspsneq	⊢ ( 𝜑 → ( ( 𝐽 ‘ { ℎ } ) = ( 𝐽 ‘ { 𝑖 } ) ↔ ∃ 𝑢 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ℎ = ( 𝑢 · 𝑖 ) ) )
33	1 3 20 21 8 26 27 12	lcdsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝐵 )
34	1 3 20 23 8 26 28 12	lcd0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = 𝑂 )
35	34	sneqd	⊢ ( 𝜑 → { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } = { 𝑂 } )
36	33 35	difeq12d	⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) = ( 𝐵 ∖ { 𝑂 } ) )
37	36	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐶 ) ) } ) ℎ = ( 𝑢 · 𝑖 ) ↔ ∃ 𝑢 ∈ ( 𝐵 ∖ { 𝑂 } ) ℎ = ( 𝑢 · 𝑖 ) ) )
38	32 37	bitrd	⊢ ( 𝜑 → ( ( 𝐽 ‘ { ℎ } ) = ( 𝐽 ‘ { 𝑖 } ) ↔ ∃ 𝑢 ∈ ( 𝐵 ∖ { 𝑂 } ) ℎ = ( 𝑢 · 𝑖 ) ) )
39	25 38	mpbid	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝐵 ∖ { 𝑂 } ) ℎ = ( 𝑢 · 𝑖 ) )