This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) = { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } )