---

Step * 1 of Lemma free-iso-int_wf


1. S : Type
2. s : S
3. ∀x,y:S.  (x = y ∈ S)
4. free-1-iso(s;ℤ-rng) ∈ free-vs(ℤ-rng;S) ≅ one-dim-vs(ℤ-rng)
⊢ free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ
BY
{ (RWO "one-dim-int-vs" (-1) THEN (Assert ⌜free-1-iso(s;ℤ-rng) = free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ⌝⋅ THENM Eq)) }

1
.....assertion..... 
1. S : Type
2. s : S
3. ∀x,y:S.  (x = y ∈ S)
4. free-1-iso(s;ℤ-rng) ∈ free-vs(ℤ-rng;S) ≅ ℤ
⊢ free-1-iso(s;ℤ-rng) = free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ

---

Latex:

---

Latex:

1.  S  :  Type
2.  s  :  S
3.  \mforall{}x,y:S.    (x  =  y)
4.  free-1-iso(s;\mBbbZ{}-rng)  \mmember{}  free-vs(\mBbbZ{}-rng;S)  \mcong{}  one-dim-vs(\mBbbZ{}-rng)
\mvdash{}  free-iso-int(s)  \mmember{}  free-vs(\mBbbZ{}-rng;S)  \mcong{}  \mBbbZ{}


By

---

Latex:
(RWO  "one-dim-int-vs"  (-1)  THEN  (Assert  \mkleeneopen{}free-1-iso(s;\mBbbZ{}-rng)  =  free-iso-int(s)\mkleeneclose{}\mcdot{}  THENM  Eq))

---

Home Index