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

Metamath Proof Explorer

Theorem diaelrnN

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

Ref Expression
Hypotheses diaelrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diaelrn.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
diaelrn.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diaelrnN ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ ran 𝐼 ) → 𝑆 ⊆ 𝑇 )

Proof

Step Hyp Ref Expression
1 diaelrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 diaelrn.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 diaelrn.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 4 5 1 3 diafn ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
7 fvelrnb ⊢ ( 𝐼 Fn { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } → ( 𝑆 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ( 𝐼 ‘ 𝑥 ) = 𝑆 ) )
8 6 7 syl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ( 𝐼 ‘ 𝑥 ) = 𝑆 ) )
9 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( le ‘ 𝐾 ) 𝑊 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
10 9 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
11 4 5 1 2 3 diass ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) ⊆ 𝑇 )
12 11 ex ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑥 ) ⊆ 𝑇 ) )
13 sseq1 ⊢ ( ( 𝐼 ‘ 𝑥 ) = 𝑆 → ( ( 𝐼 ‘ 𝑥 ) ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇 ) )
14 13 biimpcd ⊢ ( ( 𝐼 ‘ 𝑥 ) ⊆ 𝑇 → ( ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) )
15 12 14 syl6 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) ) )
16 10 15 biimtrid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } → ( ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) ) )
17 16 rexlimdv ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) )
18 8 17 sylbid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ ran 𝐼 → 𝑆 ⊆ 𝑇 ) )
19 18 imp ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ ran 𝐼 ) → 𝑆 ⊆ 𝑇 )