Step |
Hyp |
Ref |
Expression |
1 |
|
indlcim.f |
⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
indlcim.b |
⊢ 𝐵 = ( Base ‘ 𝐹 ) |
3 |
|
indlcim.c |
⊢ 𝐶 = ( Base ‘ 𝑇 ) |
4 |
|
indlcim.v |
⊢ · = ( ·𝑠 ‘ 𝑇 ) |
5 |
|
indlcim.n |
⊢ 𝑁 = ( LSpan ‘ 𝑇 ) |
6 |
|
indlcim.e |
⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) ) |
7 |
|
indlcim.t |
⊢ ( 𝜑 → 𝑇 ∈ LMod ) |
8 |
|
indlcim.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑋 ) |
9 |
|
indlcim.r |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) ) |
10 |
|
indlcim.a |
⊢ ( 𝜑 → 𝐴 : 𝐼 –onto→ 𝐽 ) |
11 |
|
indlcim.l |
⊢ ( 𝜑 → 𝐴 LIndF 𝑇 ) |
12 |
|
indlcim.s |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝐽 ) = 𝐶 ) |
13 |
|
fofn |
⊢ ( 𝐴 : 𝐼 –onto→ 𝐽 → 𝐴 Fn 𝐼 ) |
14 |
10 13
|
syl |
⊢ ( 𝜑 → 𝐴 Fn 𝐼 ) |
15 |
3
|
lindff |
⊢ ( ( 𝐴 LIndF 𝑇 ∧ 𝑇 ∈ LMod ) → 𝐴 : dom 𝐴 ⟶ 𝐶 ) |
16 |
11 7 15
|
syl2anc |
⊢ ( 𝜑 → 𝐴 : dom 𝐴 ⟶ 𝐶 ) |
17 |
16
|
frnd |
⊢ ( 𝜑 → ran 𝐴 ⊆ 𝐶 ) |
18 |
|
df-f |
⊢ ( 𝐴 : 𝐼 ⟶ 𝐶 ↔ ( 𝐴 Fn 𝐼 ∧ ran 𝐴 ⊆ 𝐶 ) ) |
19 |
14 17 18
|
sylanbrc |
⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 ) |
20 |
1 2 3 4 6 7 8 9 19
|
frlmup1 |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) ) |
21 |
1 2 3 4 6 7 8 9 19
|
islindf5 |
⊢ ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ 𝐸 : 𝐵 –1-1→ 𝐶 ) ) |
22 |
11 21
|
mpbid |
⊢ ( 𝜑 → 𝐸 : 𝐵 –1-1→ 𝐶 ) |
23 |
1 2 3 4 6 7 8 9 19 5
|
frlmup3 |
⊢ ( 𝜑 → ran 𝐸 = ( 𝑁 ‘ ran 𝐴 ) ) |
24 |
|
forn |
⊢ ( 𝐴 : 𝐼 –onto→ 𝐽 → ran 𝐴 = 𝐽 ) |
25 |
10 24
|
syl |
⊢ ( 𝜑 → ran 𝐴 = 𝐽 ) |
26 |
25
|
fveq2d |
⊢ ( 𝜑 → ( 𝑁 ‘ ran 𝐴 ) = ( 𝑁 ‘ 𝐽 ) ) |
27 |
23 26 12
|
3eqtrd |
⊢ ( 𝜑 → ran 𝐸 = 𝐶 ) |
28 |
|
dff1o5 |
⊢ ( 𝐸 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐸 : 𝐵 –1-1→ 𝐶 ∧ ran 𝐸 = 𝐶 ) ) |
29 |
22 27 28
|
sylanbrc |
⊢ ( 𝜑 → 𝐸 : 𝐵 –1-1-onto→ 𝐶 ) |
30 |
2 3
|
islmim |
⊢ ( 𝐸 ∈ ( 𝐹 LMIso 𝑇 ) ↔ ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) ∧ 𝐸 : 𝐵 –1-1-onto→ 𝐶 ) ) |
31 |
20 29 30
|
sylanbrc |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMIso 𝑇 ) ) |