Step |
Hyp |
Ref |
Expression |
1 |
|
psrsca.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psrsca.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
psrsca.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝑊 ) |
4 |
|
psrvalstr |
⊢ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) Struct 〈 1 , 9 〉 |
5 |
|
scaid |
⊢ Scalar = Slot ( Scalar ‘ ndx ) |
6 |
|
snsstp1 |
⊢ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 } ⊆ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } |
7 |
|
ssun2 |
⊢ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) |
8 |
6 7
|
sstri |
⊢ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) |
9 |
4 5 8
|
strfv |
⊢ ( 𝑅 ∈ 𝑊 → 𝑅 = ( Scalar ‘ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) ) ) |
10 |
3 9
|
syl |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) ) ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
12 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
13 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
14 |
|
eqid |
⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 ) |
15 |
|
eqid |
⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
16 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
17 |
1 11 15 16 2
|
psrbas |
⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ) |
18 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
19 |
1 16 12 18
|
psrplusg |
⊢ ( +g ‘ 𝑆 ) = ( ∘f ( +g ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ) |
20 |
|
eqid |
⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) |
21 |
1 16 13 20 15
|
psrmulr |
⊢ ( .r ‘ 𝑆 ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑧 ∈ ( Base ‘ 𝑆 ) ↦ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑤 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑧 ‘ ( 𝑤 ∘f − 𝑥 ) ) ) ) ) ) ) |
22 |
|
eqid |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) |
23 |
|
eqidd |
⊢ ( 𝜑 → ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ) |
24 |
1 11 12 13 14 15 17 19 21 22 23 2 3
|
psrval |
⊢ ( 𝜑 → 𝑆 = ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) ) |
25 |
24
|
fveq2d |
⊢ ( 𝜑 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ ( { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑆 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑅 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑓 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) 〉 } ) ) ) |
26 |
10 25
|
eqtr4d |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) ) |