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 ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) Struct ⟨ 1 , 9 ⟩
5 scaid Scalar = Slot ( Scalar ‘ ndx )
6 snsstp1 { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ⊆ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ }
7 ssun2 { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑆 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
8 6 7 sstri { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑆 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
9 4 5 8 strfv ( 𝑅𝑊𝑅 = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑆 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
10 3 9 syl ( 𝜑𝑅 = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑆 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
11 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ( +g𝑅 ) = ( +g𝑅 )
13 eqid ( .r𝑅 ) = ( .r𝑅 )
14 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
15 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
16 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
17 1 11 15 16 2 psrbas ( 𝜑 → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 ‘ 𝑆 ) ↦ ( 𝑤 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑤 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑧 ‘ ( 𝑤f𝑥 ) ) ) ) ) ) )
22 eqid ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) )
23 eqidd ( 𝜑 → ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
25 24 fveq2d ( 𝜑 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑆 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ ( Base ‘ 𝑆 ) ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
26 10 25 eqtr4d ( 𝜑𝑅 = ( Scalar ‘ 𝑆 ) )