Theorem ldual1dim

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014)

	Ref	Expression
Hypotheses	ldual1dim.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldual1dim.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
	ldual1dim.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldual1dim.n	⊢ 𝑁 = ( LSpan ‘ 𝐷 )
	ldual1dim.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	ldual1dim.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	ldual1dim	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) = { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } )

Proof

Step	Hyp	Ref	Expression
1		ldual1dim.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldual1dim.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
3		ldual1dim.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
4		ldual1dim.n	⊢ 𝑁 = ( LSpan ‘ 𝐷 )
5		ldual1dim.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		ldual1dim.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
9		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
10		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
11	7 8 3 9 10 5	ldualsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
12	11	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ↔ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
13	12	anbi1d	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) ↔ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) ) )
14		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
15		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
16		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
17	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LVec )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝐺 ∈ 𝐹 )
20	1 14 7 8 15 3 16 17 18 19	ldualvs	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) )
21	20	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ↔ 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) )
22	21	pm5.32da	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) ↔ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ) )
23	13 22	bitrd	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ) ↔ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ) )
24	23	rexbidv2	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) )
25	24	abbidv	⊢ ( 𝜑 → { 𝑔 ∣ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) } )
26		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
27	3 26	lduallmod	⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ LMod )
28	5 27	syl	⊢ ( 𝜑 → 𝐷 ∈ LMod )
29		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
30	1 3 29 5 6	ldualelvbase	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
31	9 10 29 16 4	lspsn	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑁 ‘ { 𝐺 } ) = { 𝑔 ∣ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) } )
32	28 30 31	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) = { 𝑔 ∣ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝑔 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐺 ) } )
33	14 7 1 2 8 15 5 6	lfl1dim	⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑔 = ( 𝐺 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) } )
34	25 32 33	3eqtr4d	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) = { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } )