Step |
Hyp |
Ref |
Expression |
1 |
|
f1f |
⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → 𝐹 : 𝐷 ⟶ 𝑆 ) |
2 |
|
fcoi2 |
⊢ ( 𝐹 : 𝐷 ⟶ 𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 ) |
3 |
1 2
|
syl |
⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 ) |
4 |
3
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 ) |
5 |
|
simp1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝑊 ∈ LMod ) |
6 |
|
linds2 |
⊢ ( 𝑆 ∈ ( LIndS ‘ 𝑊 ) → ( I ↾ 𝑆 ) LIndF 𝑊 ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( I ↾ 𝑆 ) LIndF 𝑊 ) |
8 |
|
dmresi |
⊢ dom ( I ↾ 𝑆 ) = 𝑆 |
9 |
|
f1eq3 |
⊢ ( dom ( I ↾ 𝑆 ) = 𝑆 → ( 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ↔ 𝐹 : 𝐷 –1-1→ 𝑆 ) ) |
10 |
8 9
|
ax-mp |
⊢ ( 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ↔ 𝐹 : 𝐷 –1-1→ 𝑆 ) |
11 |
10
|
biimpri |
⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ) |
12 |
11
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ) |
13 |
|
f1lindf |
⊢ ( ( 𝑊 ∈ LMod ∧ ( I ↾ 𝑆 ) LIndF 𝑊 ∧ 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) LIndF 𝑊 ) |
14 |
5 7 12 13
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) LIndF 𝑊 ) |
15 |
4 14
|
eqbrtrrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝐹 LIndF 𝑊 ) |