Metamath Proof Explorer


Theorem diass

Description: The value of the partial isomorphism A is a set of translations, i.e., a set of vectors. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses diass.b 𝐵 = ( Base ‘ 𝐾 )
diass.l = ( le ‘ 𝐾 )
diass.h 𝐻 = ( LHyp ‘ 𝐾 )
diass.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
diass.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diass ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ) → ( 𝐼𝑋 ) ⊆ 𝑇 )

Proof

Step Hyp Ref Expression
1 diass.b 𝐵 = ( Base ‘ 𝐾 )
2 diass.l = ( le ‘ 𝐾 )
3 diass.h 𝐻 = ( LHyp ‘ 𝐾 )
4 diass.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 diass.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6 eqid ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 1 2 3 4 6 5 diaval ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ) → ( 𝐼𝑋 ) = { 𝑓𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) 𝑋 } )
8 ssrab2 { 𝑓𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) 𝑋 } ⊆ 𝑇
9 7 8 eqsstrdi ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ) → ( 𝐼𝑋 ) ⊆ 𝑇 )