| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | suppmptcfin.f | . . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) | 
| 2 |  | eqeq1 2740 | . . . . . 6
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑋 ↔ 𝑣 = 𝑋)) | 
| 3 | 2 | ifbid 4548 | . . . . 5
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑋, 1 , 0 ) = if(𝑣 = 𝑋, 1 , 0 )) | 
| 4 | 3 | cbvmptv 5254 | . . . 4
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) | 
| 5 | 1, 4 | eqtri 2764 | . . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) | 
| 6 |  | simp2 1137 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 𝑉 ∈ 𝒫 𝐵) | 
| 7 |  | suppmptcfin.0 | . . . . 5
⊢  0 =
(0g‘𝑅) | 
| 8 | 7 | fvexi 6919 | . . . 4
⊢  0 ∈
V | 
| 9 | 8 | a1i 11 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 0 ∈ V) | 
| 10 |  | suppmptcfin.1 | . . . . . 6
⊢  1 =
(1r‘𝑅) | 
| 11 | 10 | fvexi 6919 | . . . . 5
⊢  1 ∈
V | 
| 12 | 11 | a1i 11 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 1 ∈ V) | 
| 13 | 8 | a1i 11 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 0 ∈ V) | 
| 14 | 12, 13 | ifcld 4571 | . . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → if(𝑣 = 𝑋, 1 , 0 ) ∈
V) | 
| 15 | 5, 6, 9, 14 | mptsuppd 8213 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) = {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 }) | 
| 16 |  | snfi 9084 | . . 3
⊢ {𝑋} ∈ Fin | 
| 17 |  | 2a1 28 | . . . . . 6
⊢ (𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) | 
| 18 |  | iffalse 4533 | . . . . . . . . . 10
⊢ (¬
𝑣 = 𝑋 → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) | 
| 19 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) | 
| 20 | 19 | neeq1d 2999 | . . . . . . . 8
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 ↔ 0 ≠ 0 )) | 
| 21 |  | eqid 2736 | . . . . . . . . 9
⊢  0 = 0 | 
| 22 |  | eqneqall 2950 | . . . . . . . . 9
⊢ ( 0 = 0 → (
0 ≠
0 →
𝑣 = 𝑋)) | 
| 23 | 21, 22 | ax-mp 5 | . . . . . . . 8
⊢ ( 0 ≠ 0 → 𝑣 = 𝑋) | 
| 24 | 20, 23 | biimtrdi 253 | . . . . . . 7
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) | 
| 25 | 24 | ex 412 | . . . . . 6
⊢ (¬
𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) | 
| 26 | 17, 25 | pm2.61i 182 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) | 
| 27 | 26 | ralrimiva 3145 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) | 
| 28 |  | rabsssn 4667 | . . . 4
⊢ ({𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋} ↔ ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) | 
| 29 | 27, 28 | sylibr 234 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) | 
| 30 |  | ssfi 9214 | . . 3
⊢ (({𝑋} ∈ Fin ∧ {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) | 
| 31 | 16, 29, 30 | sylancr 587 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) | 
| 32 | 15, 31 | eqeltrd 2840 | 1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) ∈
Fin) |