This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrvalstr

Description: The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion psrvalstr ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) Struct ⟨ 1 , 9 ⟩

Proof

Step Hyp Ref Expression
1 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ }
2 1 rngstr ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } Struct ⟨ 1 , 3 ⟩
3 5nn ⊢ 5 ∈ ℕ
4 scandx ⊢ ( Scalar ‘ ndx ) = 5
5 5lt6 ⊢ 5 < 6
6 6nn ⊢ 6 ∈ ℕ
7 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
8 6lt9 ⊢ 6 < 9
9 9nn ⊢ 9 ∈ ℕ
10 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
11 3 4 5 6 7 8 9 10 strle3 ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } Struct ⟨ 5 , 9 ⟩
12 3lt5 ⊢ 3 < 5
13 2 11 12 strleun ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) Struct ⟨ 1 , 9 ⟩