Step | Hyp | Ref
| Expression |
1 | | suppmptcfin.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) |
2 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑋 ↔ 𝑣 = 𝑋)) |
3 | 2 | ifbid 4438 |
. . . . 5
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑋, 1 , 0 ) = if(𝑣 = 𝑋, 1 , 0 )) |
4 | 3 | cbvmptv 5134 |
. . . 4
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) |
5 | 1, 4 | eqtri 2762 |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) |
6 | | simp2 1138 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 𝑉 ∈ 𝒫 𝐵) |
7 | | suppmptcfin.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
8 | 7 | fvexi 6691 |
. . . 4
⊢ 0 ∈
V |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 0 ∈ V) |
10 | | suppmptcfin.1 |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
11 | 10 | fvexi 6691 |
. . . . 5
⊢ 1 ∈
V |
12 | 11 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 1 ∈ V) |
13 | 8 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 0 ∈ V) |
14 | 12, 13 | ifcld 4461 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → if(𝑣 = 𝑋, 1 , 0 ) ∈
V) |
15 | 5, 6, 9, 14 | mptsuppd 7885 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) = {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 }) |
16 | | snfi 8645 |
. . 3
⊢ {𝑋} ∈ Fin |
17 | | 2a1 28 |
. . . . . 6
⊢ (𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) |
18 | | iffalse 4424 |
. . . . . . . . . 10
⊢ (¬
𝑣 = 𝑋 → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) |
19 | 18 | adantr 484 |
. . . . . . . . 9
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) |
20 | 19 | neeq1d 2994 |
. . . . . . . 8
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 ↔ 0 ≠ 0 )) |
21 | | eqid 2739 |
. . . . . . . . 9
⊢ 0 = 0 |
22 | | eqneqall 2946 |
. . . . . . . . 9
⊢ ( 0 = 0 → (
0 ≠
0 →
𝑣 = 𝑋)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ ( 0 ≠ 0 → 𝑣 = 𝑋) |
24 | 20, 23 | syl6bi 256 |
. . . . . . 7
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
25 | 24 | ex 416 |
. . . . . 6
⊢ (¬
𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) |
26 | 17, 25 | pm2.61i 185 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
27 | 26 | ralrimiva 3097 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
28 | | rabsssn 4559 |
. . . 4
⊢ ({𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋} ↔ ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
29 | 27, 28 | sylibr 237 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) |
30 | | ssfi 8775 |
. . 3
⊢ (({𝑋} ∈ Fin ∧ {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) |
31 | 16, 29, 30 | sylancr 590 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) |
32 | 15, 31 | eqeltrd 2834 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) ∈
Fin) |