Step |
Hyp |
Ref |
Expression |
1 |
|
mvrf.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
mvrf.v |
⊢ 𝑉 = ( 𝐼 mVar 𝑅 ) |
3 |
|
mvrf.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
4 |
|
mvrf.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
5 |
|
mvrf.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
6 |
|
eqid |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
7 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
8 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
9 |
2 6 7 8 4 5
|
mvrfval |
⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) |
10 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
11 |
10 8
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
12 |
5 11
|
syl |
⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
13 |
10 7
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
14 |
5 13
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
15 |
12 14
|
ifcld |
⊢ ( 𝜑 → if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) |
16 |
15
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) |
17 |
16
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
18 |
|
fvex |
⊢ ( Base ‘ 𝑅 ) ∈ V |
19 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
20 |
19
|
rabex |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V |
21 |
18 20
|
elmap |
⊢ ( ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↔ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
22 |
17 21
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
23 |
1 10 6 3 4
|
psrbas |
⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
25 |
22 24
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐵 ) |
26 |
9 25
|
fmpt3d |
⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 ) |