Metamath Proof Explorer


Theorem dia1dim2

Description: Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim2.h 𝐻 = ( LHyp ‘ 𝐾 )
dia1dim2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia1dim2.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dva1dim2.u 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dia1dim2.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
dva1dim2.n 𝑁 = ( LSpan ‘ 𝑈 )
Assertion dia1dim2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )

Proof

Step Hyp Ref Expression
1 dia1dim2.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1dim2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dia1dim2.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4 dva1dim2.u 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
5 dia1dim2.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6 dva1dim2.n 𝑁 = ( LSpan ‘ 𝑈 )
7 eqid ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
9 eqid ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
10 1 7 4 8 9 dvabase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
11 10 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 rexeqdv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) ) )
13 eqid ( ·𝑠𝑈 ) = ( ·𝑠𝑈 )
14 1 2 7 4 13 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹𝑇 ) ) → ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) = ( 𝑠𝐹 ) )
15 14 anass1rs ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) = ( 𝑠𝐹 ) )
16 15 eqeq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) ↔ 𝑔 = ( 𝑠𝐹 ) ) )
17 16 rexbidva ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠𝐹 ) ) )
18 12 17 bitrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠𝐹 ) ) )
19 18 abbidv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) } = { 𝑔 ∣ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠𝐹 ) } )
20 1 4 dvalvec ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ LVec )
21 20 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝑈 ∈ LVec )
22 lveclmod ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
23 21 22 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝑈 ∈ LMod )
24 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹𝑇 )
25 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
26 1 2 4 25 dvavbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝑈 ) = 𝑇 )
27 26 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( Base ‘ 𝑈 ) = 𝑇 )
28 24 27 eleqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( Base ‘ 𝑈 ) )
29 8 9 25 13 6 lspsn ( ( 𝑈 ∈ LMod ∧ 𝐹 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝐹 } ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) } )
30 23 28 29 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑁 ‘ { 𝐹 } ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠𝑈 ) 𝐹 ) } )
31 1 2 3 7 5 dia1dim ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠𝐹 ) } )
32 19 30 31 3eqtr4rd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )