Step |
Hyp |
Ref |
Expression |
1 |
|
lnrfg.s |
⊢ 𝑆 = ( Scalar ‘ 𝑀 ) |
2 |
|
eqid |
⊢ ( 𝑆 freeLMod 𝑎 ) = ( 𝑆 freeLMod 𝑎 ) |
3 |
|
eqid |
⊢ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) = ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
5 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 ) |
6 |
|
eqid |
⊢ ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) |
7 |
|
fglmod |
⊢ ( 𝑀 ∈ LFinGen → 𝑀 ∈ LMod ) |
8 |
7
|
ad3antrrr |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod ) |
9 |
|
vex |
⊢ 𝑎 ∈ V |
10 |
9
|
a1i |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ V ) |
11 |
1
|
a1i |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 = ( Scalar ‘ 𝑀 ) ) |
12 |
|
f1oi |
⊢ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 |
13 |
|
f1of |
⊢ ( ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 → ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 ) |
14 |
12 13
|
ax-mp |
⊢ ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 |
15 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → 𝑎 ⊆ ( Base ‘ 𝑀 ) ) |
16 |
|
fss |
⊢ ( ( ( I ↾ 𝑎 ) : 𝑎 ⟶ 𝑎 ∧ 𝑎 ⊆ ( Base ‘ 𝑀 ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) ) |
17 |
14 15 16
|
sylancr |
⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) ) |
18 |
17
|
ad2antlr |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( I ↾ 𝑎 ) : 𝑎 ⟶ ( Base ‘ 𝑀 ) ) |
19 |
2 3 4 5 6 8 10 11 18
|
frlmup1 |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) ) |
20 |
|
simpllr |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑆 ∈ LNoeR ) |
21 |
|
simprl |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑎 ∈ Fin ) |
22 |
2
|
lnrfrlm |
⊢ ( ( 𝑆 ∈ LNoeR ∧ 𝑎 ∈ Fin ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM ) |
23 |
20 21 22
|
syl2anc |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM ) |
24 |
|
eqid |
⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 ) |
25 |
2 3 4 5 6 8 10 11 18 24
|
frlmup3 |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) ) |
26 |
|
rnresi |
⊢ ran ( I ↾ 𝑎 ) = 𝑎 |
27 |
26
|
fveq2i |
⊢ ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) |
28 |
|
simprr |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) |
29 |
27 28
|
syl5eq |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ( ( LSpan ‘ 𝑀 ) ‘ ran ( I ↾ 𝑎 ) ) = ( Base ‘ 𝑀 ) ) |
30 |
25 29
|
eqtrd |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) ) |
31 |
4
|
lnmepi |
⊢ ( ( ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) ∈ ( ( 𝑆 freeLMod 𝑎 ) LMHom 𝑀 ) ∧ ( 𝑆 freeLMod 𝑎 ) ∈ LNoeM ∧ ran ( 𝑏 ∈ ( Base ‘ ( 𝑆 freeLMod 𝑎 ) ) ↦ ( 𝑀 Σg ( 𝑏 ∘f ( ·𝑠 ‘ 𝑀 ) ( I ↾ 𝑎 ) ) ) ) = ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LNoeM ) |
32 |
19 23 30 31
|
syl3anc |
⊢ ( ( ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) ∧ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LNoeM ) |
33 |
4 24
|
islmodfg |
⊢ ( 𝑀 ∈ LMod → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) ) |
34 |
7 33
|
syl |
⊢ ( 𝑀 ∈ LFinGen → ( 𝑀 ∈ LFinGen ↔ ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) ) |
35 |
34
|
ibi |
⊢ ( 𝑀 ∈ LFinGen → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) |
36 |
35
|
adantr |
⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → ∃ 𝑎 ∈ 𝒫 ( Base ‘ 𝑀 ) ( 𝑎 ∈ Fin ∧ ( ( LSpan ‘ 𝑀 ) ‘ 𝑎 ) = ( Base ‘ 𝑀 ) ) ) |
37 |
32 36
|
r19.29a |
⊢ ( ( 𝑀 ∈ LFinGen ∧ 𝑆 ∈ LNoeR ) → 𝑀 ∈ LNoeM ) |