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 ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. ( TopSet ` ndx ) , J >. } ) Struct <. 1 , 9 >.

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. }
2 1 rngstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } Struct <. 1 , 3 >.
3 5nn 
 |-  5 e. NN
4 scandx 
 |-  ( Scalar ` ndx ) = 5
5 5lt6 
 |-  5 < 6
6 6nn 
 |-  6 e. NN
7 vscandx 
 |-  ( .s ` ndx ) = 6
8 6lt9 
 |-  6 < 9
9 9nn 
 |-  9 e. NN
10 tsetndx 
 |-  ( TopSet ` ndx ) = 9
11 3 4 5 6 7 8 9 10 strle3 
 |-  { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. ( TopSet ` ndx ) , J >. } Struct <. 5 , 9 >.
12 3lt5 
 |-  3 < 5
13 2 11 12 strleun 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. ( TopSet ` ndx ) , J >. } ) Struct <. 1 , 9 >.