Theorem hgmapval0

Description: Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hgmapval0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hgmapval0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hgmapval0.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hgmapval0.o	⊢ 0 = ( 0g ‘ 𝑅 )
	hgmapval0.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hgmapval0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hgmapval0	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		hgmapval0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hgmapval0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hgmapval0.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4		hgmapval0.o	⊢ 0 = ( 0g ‘ 𝑅 )
5		hgmapval0.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
6		hgmapval0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
8		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
9	1 2 7 8 6	dvh1dim	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) 𝑥 ≠ ( 0g ‘ 𝑈 ) )
10		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
12		eqid	⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ 𝑈 ) )
15	1 2 7 8 10 11 12 13 14	hdmapeq0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑥 = ( 0g ‘ 𝑈 ) ) )
16	15	biimpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 = ( 0g ‘ 𝑈 ) ) )
17	16	necon3ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑥 ≠ ( 0g ‘ 𝑈 ) → ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
18	17	3impia	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
19	1 2 6	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
21	7 3 20 4 8	lmod0vs	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) = ( 0g ‘ 𝑈 ) )
22	19 21	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) = ( 0g ‘ 𝑈 ) )
23	22	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) = ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) )
24		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25		eqid	⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
26	3 24 4	lmod0cl	⊢ ( 𝑈 ∈ LMod → 0 ∈ ( Base ‘ 𝑅 ) )
27	19 26	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
29	1 2 7 20 3 24 10 25 12 5 13 14 28	hgmapvs	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) = ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
30	1 2 8 10 11 12 6	hdmapval0	⊢ ( 𝜑 → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
32	23 29 31	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
33		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
34		eqid	⊢ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
35		eqid	⊢ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
36		eqid	⊢ ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
37	1 10 6	lcdlvec	⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
39	1 2 13	dvhlmod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
40	39 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
41	1 2 3 24 10 34 35 5 13 40	hgmapdcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐺 ‘ 0 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
42	1 2 7 10 33 12 13 14	hdmapcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
43	33 25 34 35 36 11 38 41 42	lvecvs0or	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∨ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
44	32 43	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∨ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
45	44	orcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∨ ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
46	45	ord	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
47	46	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ( ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
48	18 47	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
49	48	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) 𝑥 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
50	9 49	mpd	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
51	1 2 3 4 10 34 36 6	lcd0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = 0 )
52	50 51	eqtrd	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )