Metamath Proof Explorer


Theorem dia1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in Crawley p. 120 line 21. (Contributed by NM, 15-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim.h 𝐻 = ( LHyp ‘ 𝐾 )
dia1dim.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia1dim.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia1dim.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dia1dim.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dia1dim ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔 ∣ ∃ 𝑠𝐸 𝑔 = ( 𝑠𝐹 ) } )

Proof

Step Hyp Ref Expression
1 dia1dim.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1dim.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dia1dim.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4 dia1dim.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 dia1dim.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 1 2 3 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) )
9 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
10 9 1 2 3 trlle ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝑅𝐹 ) ( le ‘ 𝐾 ) 𝑊 )
11 7 9 1 2 3 5 diaval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑅𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅𝐹 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔𝑇 ∣ ( 𝑅𝑔 ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) } )
12 6 8 10 11 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔𝑇 ∣ ( 𝑅𝑔 ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) } )
13 9 1 2 3 4 dva1dim ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → { 𝑔 ∣ ∃ 𝑠𝐸 𝑔 = ( 𝑠𝐹 ) } = { 𝑔𝑇 ∣ ( 𝑅𝑔 ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) } )
14 12 13 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = { 𝑔 ∣ ∃ 𝑠𝐸 𝑔 = ( 𝑠𝐹 ) } )