Theorem hdmap14lem14

Description: Part of proof of part 14 in Baer p. 50 line 3. (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 ‘ 𝑃 )
Assertion	hdmap14lem14	⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) )

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		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15	1 2 3 14 10	dvh1dim	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑉 𝑦 ≠ ( 0g ‘ 𝑈 ) )
16	10	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17		3simpc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) )
18		eldifsn	⊢ ( 𝑦 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) )
19	17 18	sylibr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → 𝑦 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
20	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → 𝐹 ∈ 𝐵 )
21	1 2 3 4 14 5 6 7 8 12 13 9 16 19 20	hdmap14lem7	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
22		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝜑 )
23	22 10	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24	22 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝐹 ∈ 𝐵 )
25	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝑦 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
26		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ 𝐴 )
27	1 2 3 4 5 6 7 8 9 23 24 12 13 14 25 26	hdmap14lem13	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) ∧ 𝑔 ∈ 𝐴 ) → ( ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
28	27	reubidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → ( ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ↔ ∃! 𝑔 ∈ 𝐴 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
29	21 28	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ≠ ( 0g ‘ 𝑈 ) ) → ∃! 𝑔 ∈ 𝐴 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) )
30	29	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑉 𝑦 ≠ ( 0g ‘ 𝑈 ) → ∃! 𝑔 ∈ 𝐴 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
31	15 30	mpd	⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) )