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	syl5bi	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } → ( ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) ) )
17	16	rexlimdv	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ( 𝐼 ‘ 𝑥 ) = 𝑆 → 𝑆 ⊆ 𝑇 ) )
18	8 17	sylbid	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ ran 𝐼 → 𝑆 ⊆ 𝑇 ) )
19	18	imp	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ ran 𝐼 ) → 𝑆 ⊆ 𝑇 )