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 ⊢ H = LHyp ⁡ K
diaelrn.t ⊢ T = LTrn ⁡ K ⁡ W
diaelrn.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diaelrnN ⊢ K ∈ V ∧ W ∈ H ∧ S ∈ ran ⁡ I → S ⊆ T

Proof

Step Hyp Ref Expression
1 diaelrn.h ⊢ H = LHyp ⁡ K
2 diaelrn.t ⊢ T = LTrn ⁡ K ⁡ W
3 diaelrn.i ⊢ I = DIsoA ⁡ K ⁡ W
4 eqid ⊢ Base K = Base K
5 eqid ⊢ ≤ K = ≤ K
6 4 5 1 3 diafn ⊢ K ∈ V ∧ W ∈ H → I Fn y ∈ Base K | y ≤ K W
7 fvelrnb ⊢ I Fn y ∈ Base K | y ≤ K W → S ∈ ran ⁡ I ↔ ∃ x ∈ y ∈ Base K | y ≤ K W I ⁡ x = S
8 6 7 syl ⊢ K ∈ V ∧ W ∈ H → S ∈ ran ⁡ I ↔ ∃ x ∈ y ∈ Base K | y ≤ K W I ⁡ x = S
9 breq1 ⊢ y = x → y ≤ K W ↔ x ≤ K W
10 9 elrab ⊢ x ∈ y ∈ Base K | y ≤ K W ↔ x ∈ Base K ∧ x ≤ K W
11 4 5 1 2 3 diass ⊢ K ∈ V ∧ W ∈ H ∧ x ∈ Base K ∧ x ≤ K W → I ⁡ x ⊆ T
12 11 ex ⊢ K ∈ V ∧ W ∈ H → x ∈ Base K ∧ x ≤ K W → I ⁡ x ⊆ T
13 sseq1 ⊢ I ⁡ x = S → I ⁡ x ⊆ T ↔ S ⊆ T
14 13 biimpcd ⊢ I ⁡ x ⊆ T → I ⁡ x = S → S ⊆ T
15 12 14 syl6 ⊢ K ∈ V ∧ W ∈ H → x ∈ Base K ∧ x ≤ K W → I ⁡ x = S → S ⊆ T
16 10 15 syl5bi ⊢ K ∈ V ∧ W ∈ H → x ∈ y ∈ Base K | y ≤ K W → I ⁡ x = S → S ⊆ T
17 16 rexlimdv ⊢ K ∈ V ∧ W ∈ H → ∃ x ∈ y ∈ Base K | y ≤ K W I ⁡ x = S → S ⊆ T
18 8 17 sylbid ⊢ K ∈ V ∧ W ∈ H → S ∈ ran ⁡ I → S ⊆ T
19 18 imp ⊢ K ∈ V ∧ W ∈ H ∧ S ∈ ran ⁡ I → S ⊆ T