Step | Hyp | Ref
| Expression |
1 | | suppmptcfin.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) |
2 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑋 ↔ 𝑣 = 𝑋)) |
3 | 2 | ifbid 4108 |
. . . . 5
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑋, 1 , 0 ) = if(𝑣 = 𝑋, 1 , 0 )) |
4 | 3 | cbvmptv 4750 |
. . . 4
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) |
5 | 1, 4 | eqtri 2644 |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉 ↦ if(𝑣 = 𝑋, 1 , 0 )) |
6 | | simp2 1062 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 𝑉 ∈ 𝒫 𝐵) |
7 | | suppmptcfin.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
8 | | fvex 6201 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
9 | 7, 8 | eqeltri 2697 |
. . . 4
⊢ 0 ∈
V |
10 | 9 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → 0 ∈ V) |
11 | | suppmptcfin.1 |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
12 | | fvex 6201 |
. . . . . 6
⊢
(1r‘𝑅) ∈ V |
13 | 11, 12 | eqeltri 2697 |
. . . . 5
⊢ 1 ∈
V |
14 | 13 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 1 ∈ V) |
15 | 9 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → 0 ∈ V) |
16 | 14, 15 | ifcld 4131 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → if(𝑣 = 𝑋, 1 , 0 ) ∈
V) |
17 | 5, 6, 10, 16 | mptsuppd 7318 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) = {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 }) |
18 | | snfi 8038 |
. . 3
⊢ {𝑋} ∈ Fin |
19 | | 2a1 28 |
. . . . . 6
⊢ (𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) |
20 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑣 = 𝑋 → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) |
21 | 20 | adantr 481 |
. . . . . . . . 9
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → if(𝑣 = 𝑋, 1 , 0 ) = 0 ) |
22 | 21 | neeq1d 2853 |
. . . . . . . 8
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 ↔ 0 ≠ 0 )) |
23 | | eqid 2622 |
. . . . . . . . 9
⊢ 0 = 0 |
24 | | eqneqall 2805 |
. . . . . . . . 9
⊢ ( 0 = 0 → (
0 ≠
0 →
𝑣 = 𝑋)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . 8
⊢ ( 0 ≠ 0 → 𝑣 = 𝑋) |
26 | 22, 25 | syl6bi 243 |
. . . . . . 7
⊢ ((¬
𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
27 | 26 | ex 450 |
. . . . . 6
⊢ (¬
𝑣 = 𝑋 → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋))) |
28 | 19, 27 | pm2.61i 176 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) → (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
29 | 28 | ralrimiva 2966 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
30 | | rabsssn 4215 |
. . . 4
⊢ ({𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋} ↔ ∀𝑣 ∈ 𝑉 (if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 → 𝑣 = 𝑋)) |
31 | 29, 30 | sylibr 224 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) |
32 | | ssfi 8180 |
. . 3
⊢ (({𝑋} ∈ Fin ∧ {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ⊆ {𝑋}) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) |
33 | 18, 31, 32 | sylancr 695 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → {𝑣 ∈ 𝑉 ∣ if(𝑣 = 𝑋, 1 , 0 ) ≠ 0 } ∈
Fin) |
34 | 17, 33 | eqeltrd 2701 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 supp 0 ) ∈
Fin) |