Step |
Hyp |
Ref |
Expression |
1 |
|
psdcl.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psdcl.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
3 |
|
psdcl.r |
⊢ ( 𝜑 → 𝑅 ∈ Mgm ) |
4 |
|
psdcl.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
5 |
|
psdcl.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) |
6 |
|
fvexd |
⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V ) |
7 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
8 |
7
|
rabex |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V |
9 |
8
|
a1i |
⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V ) |
10 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Mgm ) |
11 |
|
eqid |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
12 |
11
|
psrbagf |
⊢ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑘 : 𝐼 ⟶ ℕ0 ) |
13 |
12
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑘 : 𝐼 ⟶ ℕ0 ) |
14 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑋 ∈ 𝐼 ) |
15 |
13 14
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ‘ 𝑋 ) ∈ ℕ0 ) |
16 |
|
nn0p1nn |
⊢ ( ( 𝑘 ‘ 𝑋 ) ∈ ℕ0 → ( ( 𝑘 ‘ 𝑋 ) + 1 ) ∈ ℕ ) |
17 |
15 16
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑘 ‘ 𝑋 ) + 1 ) ∈ ℕ ) |
18 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
19 |
1 18 11 2 5
|
psrelbas |
⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
20 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
21 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
22 |
|
reldmpsr |
⊢ Rel dom mPwSer |
23 |
1 2 22
|
strov2rcl |
⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V ) |
24 |
5 23
|
syl |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
25 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
26 |
11
|
snifpsrbag |
⊢ ( ( 𝐼 ∈ V ∧ 1 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
27 |
24 25 26
|
sylancl |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
28 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
29 |
11
|
psrbagaddcl |
⊢ ( ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
30 |
21 28 29
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) |
31 |
20 30
|
ffvelcdmd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
32 |
|
eqid |
⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 ) |
33 |
18 32
|
mulgnncl |
⊢ ( ( 𝑅 ∈ Mgm ∧ ( ( 𝑘 ‘ 𝑋 ) + 1 ) ∈ ℕ ∧ ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
34 |
10 17 31 33
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
35 |
34
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
36 |
6 9 35
|
elmapdd |
⊢ ( 𝜑 → ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
37 |
1 2 11 4 5
|
psdval |
⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) |
38 |
1 18 11 2 24
|
psrbas |
⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
39 |
36 37 38
|
3eltr4d |
⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 ) |