Metamath Proof Explorer

Theorem pwsle

Description: Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015)

Ref Expression
Hypotheses pwsle.y 
|- Y = ( R ^s I )
pwsle.v 
|- B = ( Base ` Y )
pwsle.o 
|- O = ( le ` R )
pwsle.l 
|- .<_ = ( le ` Y )
Assertion pwsle 
|- ( ( R e. V /\ I e. W ) -> .<_ = ( oR O i^i ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 pwsle.y 
 |-  Y = ( R ^s I )
2 pwsle.v 
 |-  B = ( Base ` Y )
3 pwsle.o 
 |-  O = ( le ` R )
4 pwsle.l 
 |-  .<_ = ( le ` Y )
5 vex 
 |-  f e. _V
6 vex 
 |-  g e. _V
7 5 6 prss 
 |-  ( ( f e. B /\ g e. B ) <-> { f , g } C_ B )
8 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
9 1 8 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
10 9 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
11 2 10 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> B = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
12 11 sseq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( { f , g } C_ B <-> { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) )
13 7 12 syl5bb 
 |-  ( ( R e. V /\ I e. W ) -> ( ( f e. B /\ g e. B ) <-> { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ) )
14 13 anbi1d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) <-> ( { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) ) )
15 fvconst2g 
 |-  ( ( R e. V /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
16 15 ad4ant14 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
17 16 fveq2d 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( le ` ( ( I X. { R } ) ` x ) ) = ( le ` R ) )
18 17 3 eqtr4di 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( le ` ( ( I X. { R } ) ` x ) ) = O )
19 18 breqd 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) <-> ( f ` x ) O ( g ` x ) ) )
20 19 ralbidva 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> ( A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) <-> A. x e. I ( f ` x ) O ( g ` x ) ) )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 simpll 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> R e. V )
23 simplr 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> I e. W )
24 simprl 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> f e. B )
25 1 21 2 22 23 24 pwselbas 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> f : I --> ( Base ` R ) )
26 25 ffnd 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> f Fn I )
27 simprr 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> g e. B )
28 1 21 2 22 23 27 pwselbas 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> g : I --> ( Base ` R ) )
29 28 ffnd 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> g Fn I )
30 inidm 
 |-  ( I i^i I ) = I
31 eqidd 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( f ` x ) = ( f ` x ) )
32 eqidd 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
33 26 29 24 27 30 31 32 ofrfvalg 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> ( f oR O g <-> A. x e. I ( f ` x ) O ( g ` x ) ) )
34 20 33 bitr4d 
 |-  ( ( ( R e. V /\ I e. W ) /\ ( f e. B /\ g e. B ) ) -> ( A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) <-> f oR O g ) )
35 34 pm5.32da 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) <-> ( ( f e. B /\ g e. B ) /\ f oR O g ) ) )
36 brinxp2 
 |-  ( f ( oR O i^i ( B X. B ) ) g <-> ( ( f e. B /\ g e. B ) /\ f oR O g ) )
37 35 36 bitr4di 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) <-> f ( oR O i^i ( B X. B ) ) g ) )
38 14 37 bitr3d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) <-> f ( oR O i^i ( B X. B ) ) g ) )
39 38 opabbidv 
 |-  ( ( R e. V /\ I e. W ) -> { <. f , g >. | ( { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) } = { <. f , g >. | f ( oR O i^i ( B X. B ) ) g } )
40 9 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( le ` Y ) = ( le ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
41 4 40 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> .<_ = ( le ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
42 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
43 fvexd 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` R ) e. _V )
44 simpr 
 |-  ( ( R e. V /\ I e. W ) -> I e. W )
45 snex 
 |-  { R } e. _V
46 xpexg 
 |-  ( ( I e. W /\ { R } e. _V ) -> ( I X. { R } ) e. _V )
47 44 45 46 sylancl 
 |-  ( ( R e. V /\ I e. W ) -> ( I X. { R } ) e. _V )
48 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
49 snnzg 
 |-  ( R e. V -> { R } =/= (/) )
50 49 adantr 
 |-  ( ( R e. V /\ I e. W ) -> { R } =/= (/) )
51 dmxp 
 |-  ( { R } =/= (/) -> dom ( I X. { R } ) = I )
52 50 51 syl 
 |-  ( ( R e. V /\ I e. W ) -> dom ( I X. { R } ) = I )
53 eqid 
 |-  ( le ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( le ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
54 42 43 47 48 52 53 prdsle 
 |-  ( ( R e. V /\ I e. W ) -> ( le ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = { <. f , g >. | ( { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) } )
55 41 54 eqtrd 
 |-  ( ( R e. V /\ I e. W ) -> .<_ = { <. f , g >. | ( { f , g } C_ ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) /\ A. x e. I ( f ` x ) ( le ` ( ( I X. { R } ) ` x ) ) ( g ` x ) ) } )
56 relinxp 
 |-  Rel ( oR O i^i ( B X. B ) )
57 56 a1i 
 |-  ( ( R e. V /\ I e. W ) -> Rel ( oR O i^i ( B X. B ) ) )
58 dfrel4v 
 |-  ( Rel ( oR O i^i ( B X. B ) ) <-> ( oR O i^i ( B X. B ) ) = { <. f , g >. | f ( oR O i^i ( B X. B ) ) g } )
59 57 58 sylib 
 |-  ( ( R e. V /\ I e. W ) -> ( oR O i^i ( B X. B ) ) = { <. f , g >. | f ( oR O i^i ( B X. B ) ) g } )
60 39 55 59 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> .<_ = ( oR O i^i ( B X. B ) ) )