Theorem hdmap14lem12

Description: Lemma for proof of part 14 in Baer p. 50. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap14lem12.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem12.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap14lem12.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hdmap14lem12.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmap14lem12.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmap14lem12.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem12.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	hdmap14lem12.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap14lem12.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap14lem12.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	hdmap14lem12.p	⊢ 𝑃 = ( Scalar ‘ 𝐶 )
	hdmap14lem12.a	⊢ 𝐴 = ( Base ‘ 𝑃 )
	hdmap14lem12.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmap14lem12.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	hdmap14lem12.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
Assertion	hdmap14lem12	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap14lem12.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap14lem12.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap14lem12.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
5		hdmap14lem12.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		hdmap14lem12.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
7		hdmap14lem12.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap14lem12.e	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9		hdmap14lem12.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10		hdmap14lem12.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		hdmap14lem12.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
12		hdmap14lem12.p	⊢ 𝑃 = ( Scalar ‘ 𝐶 )
13		hdmap14lem12.a	⊢ 𝐴 = ( Base ‘ 𝑃 )
14		hdmap14lem12.o	⊢ 0 = ( 0g ‘ 𝑈 )
15		hdmap14lem12.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
16		hdmap14lem12.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
17		eqid	⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
18	10	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19		simp3	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
20	19	eldifad	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑦 ∈ 𝑉 )
21	11	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝐹 ∈ 𝐵 )
22	1 2 3 4 5 6 7 8 17 12 13 9 18 20 21	hdmap14lem2a	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
23		simp3	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
24		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
25		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
26		eqid	⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
27		simp11	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝜑 )
28	27 10	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29	27 15	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
30		simp13	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
31	27 11	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐹 ∈ 𝐵 )
32	27 16	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐺 ∈ 𝐴 )
33		simp2	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑔 ∈ 𝐴 )
34		simp12	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
35	1 2 3 24 4 14 25 5 6 7 26 8 12 13 9 28 29 30 31 32 33 34 23	hdmap14lem11	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐺 = 𝑔 )
36	35	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
37	23 36	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
38	37	rexlimdv3a	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )
39	22 38	mpd	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
40	39	3expia	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )
41	40	ralrimiv	⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
42		oveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 · 𝑦 ) = ( 𝐹 · 𝑋 ) )
43	42	fveq2d	⊢ ( 𝑦 = 𝑋 → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) )
44		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑋 ) )
45	44	oveq2d	⊢ ( 𝑦 = 𝑋 → ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
46	43 45	eqeq12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
47	46	rspcv	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → ( ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
48	15 47	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
49	48	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
50	41 49	impbida	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )