Theorem hdmap14lem2a

Description: Prior to part 14 in Baer p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 . (Contributed by NM, 31-May-2015)

	Ref	Expression
Hypotheses	hdmap14lem1a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap14lem1a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem1a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap14lem1a.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hdmap14lem1a.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmap14lem1a.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmap14lem1a.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem2a.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	hdmap14lem1a.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
	hdmap14lem2a.p	⊢ 𝑃 = ( Scalar ‘ 𝐶 )
	hdmap14lem2a.a	⊢ 𝐴 = ( Base ‘ 𝑃 )
	hdmap14lem1a.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem1a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap14lem3a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmap14lem1a.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	hdmap14lem2a	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap14lem1a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap14lem1a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap14lem1a.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
5		hdmap14lem1a.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		hdmap14lem1a.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
7		hdmap14lem1a.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap14lem2a.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9		hdmap14lem1a.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
10		hdmap14lem2a.p	⊢ 𝑃 = ( Scalar ‘ 𝐶 )
11		hdmap14lem2a.a	⊢ 𝐴 = ( Base ‘ 𝑃 )
12		hdmap14lem1a.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
13		hdmap14lem1a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		hdmap14lem3a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15		hdmap14lem1a.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
16		fvoveq1	⊢ ( 𝐹 = ( 0g ‘ 𝑅 ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) )
17	16	eqeq1d	⊢ ( 𝐹 = ( 0g ‘ 𝑅 ) → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
18	17	rexbidv	⊢ ( 𝐹 = ( 0g ‘ 𝑅 ) → ( ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
19		difss	⊢ ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ⊆ 𝐴
20	13	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21	14	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ 𝑉 )
22	15	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → 𝐹 ∈ 𝐵 )
23		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → 𝐹 ≠ ( 0g ‘ 𝑅 ) )
25	1 2 3 4 5 6 7 8 9 10 11 12 20 21 22 23 24	hdmap14lem1a	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐿 ‘ { ( 𝑆 ‘ 𝑋 ) } ) = ( 𝐿 ‘ { ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) } ) )
26	25	eqcomd	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐿 ‘ { ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) } ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑋 ) } ) )
27		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
28		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
29	1 7 13	lcdlvec	⊢ ( 𝜑 → 𝐶 ∈ LVec )
30	1 2 13	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
31	3 5 4 6	lmodvscl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 · 𝑋 ) ∈ 𝑉 )
32	30 15 14 31	syl3anc	⊢ ( 𝜑 → ( 𝐹 · 𝑋 ) ∈ 𝑉 )
33	1 2 3 7 27 12 13 32	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) ∈ ( Base ‘ 𝐶 ) )
34	1 2 3 7 27 12 13 14	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
35	27 10 11 28 8 9 29 33 34	lspsneq	⊢ ( 𝜑 → ( ( 𝐿 ‘ { ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) } ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑋 ) } ) ↔ ∃ 𝑔 ∈ ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐿 ‘ { ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) } ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑋 ) } ) ↔ ∃ 𝑔 ∈ ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
37	26 36	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑔 ∈ ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
38		ssrexv	⊢ ( ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ⊆ 𝐴 → ( ∃ 𝑔 ∈ ( 𝐴 ∖ { ( 0g ‘ 𝑃 ) } ) ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
39	19 37 38	mpsyl	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
40	1 7 13	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
41	10 11 28	lmod0cl	⊢ ( 𝐶 ∈ LMod → ( 0g ‘ 𝑃 ) ∈ 𝐴 )
42	40 41	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐴 )
43		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
44		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
45	1 2 43 7 44 12 13	hdmapval0	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝐶 ) )
46	3 5 4 23 43	lmod0vs	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑈 ) )
47	30 14 46	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑈 ) )
48	47	fveq2d	⊢ ( 𝜑 → ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) )
49	27 10 8 28 44	lmod0vs	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( 0g ‘ 𝑃 ) ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
50	40 34 49	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
51	45 48 50	3eqtr4d	⊢ ( 𝜑 → ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( ( 0g ‘ 𝑃 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
52		oveq1	⊢ ( 𝑔 = ( 0g ‘ 𝑃 ) → ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( ( 0g ‘ 𝑃 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
53	52	rspceeqv	⊢ ( ( ( 0g ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( ( 0g ‘ 𝑃 ) ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
54	42 51 53	syl2anc	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
55	18 39 54	pm2.61ne	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )