Metamath Proof Explorer

Theorem psrsca

Description: The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrsca.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrsca.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrsca.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion psrsca ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )

Proof

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 ‘ 𝑆 ) )