Metamath Proof Explorer

Theorem imasvalstr

Description: Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypothesis imasvalstr.u 
|- U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } )
Assertion imasvalstr 
|- U Struct <. 1 , ; 1 2 >.

Proof

Step Hyp Ref Expression
1 imasvalstr.u 
 |-  U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } )
2 eqid 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )
3 2 ipsstr 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) Struct <. 1 , 8 >.
4 9nn 
 |-  9 e. NN
5 tsetndx 
 |-  ( TopSet ` ndx ) = 9
6 9lt10 
 |-  9 < ; 1 0
7 10nn 
 |-  ; 1 0 e. NN
8 plendx 
 |-  ( le ` ndx ) = ; 1 0
9 1nn0 
 |-  1 e. NN0
10 0nn0 
 |-  0 e. NN0
11 2nn 
 |-  2 e. NN
12 2pos 
 |-  0 < 2
13 9 10 11 12 declt 
 |-  ; 1 0 < ; 1 2
14 9 11 decnncl 
 |-  ; 1 2 e. NN
15 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
16 4 5 6 7 8 13 14 15 strle3 
 |-  { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } Struct <. 9 , ; 1 2 >.
17 8lt9 
 |-  8 < 9
18 3 16 17 strleun 
 |-  ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } ) Struct <. 1 , ; 1 2 >.
19 1 18 eqbrtri 
 |-  U Struct <. 1 , ; 1 2 >.