Metamath Proof Explorer

Theorem xpsmul

Description: Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses xpsval.t 
|- T = ( R Xs. S )
xpsval.x 
|- X = ( Base ` R )
xpsval.y 
|- Y = ( Base ` S )
xpsval.1 
|- ( ph -> R e. V )
xpsval.2 
|- ( ph -> S e. W )
xpsadd.3 
|- ( ph -> A e. X )
xpsadd.4 
|- ( ph -> B e. Y )
xpsadd.5 
|- ( ph -> C e. X )
xpsadd.6 
|- ( ph -> D e. Y )
xpsadd.7 
|- ( ph -> ( A .x. C ) e. X )
xpsadd.8 
|- ( ph -> ( B .X. D ) e. Y )
xpsmul.m 
|- .x. = ( .r ` R )
xpsmul.n 
|- .X. = ( .r ` S )
xpsmul.p 
|- .xb = ( .r ` T )
Assertion xpsmul 
|- ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )

Proof

Step Hyp Ref Expression
1 xpsval.t 
 |-  T = ( R Xs. S )
2 xpsval.x 
 |-  X = ( Base ` R )
3 xpsval.y 
 |-  Y = ( Base ` S )
4 xpsval.1 
 |-  ( ph -> R e. V )
5 xpsval.2 
 |-  ( ph -> S e. W )
6 xpsadd.3 
 |-  ( ph -> A e. X )
7 xpsadd.4 
 |-  ( ph -> B e. Y )
8 xpsadd.5 
 |-  ( ph -> C e. X )
9 xpsadd.6 
 |-  ( ph -> D e. Y )
10 xpsadd.7 
 |-  ( ph -> ( A .x. C ) e. X )
11 xpsadd.8 
 |-  ( ph -> ( B .X. D ) e. Y )
12 xpsmul.m 
 |-  .x. = ( .r ` R )
13 xpsmul.n 
 |-  .X. = ( .r ` S )
14 xpsmul.p 
 |-  .xb = ( .r ` T )
15 eqid 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
16 eqid 
 |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
17 15 xpsff1o2 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
18 f1ocnv 
 |-  ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
19 17 18 mp1i 
 |-  ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
20 f1ofo 
 |-  ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( X X. Y ) )
21 19 20 syl 
 |-  ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( X X. Y ) )
22 19 f1ocpbl 
 |-  ( ( ph /\ ( a e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ b e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) /\ ( c e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ d e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) -> ( ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` a ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` c ) /\ ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` b ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` d ) ) -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( a ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) b ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( c ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) d ) ) ) )
23 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
24 1 2 3 4 5 15 23 16 xpsval 
 |-  ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
25 1 2 3 4 5 15 23 16 xpsrnbas 
 |-  ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
26 ovexd 
 |-  ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
27 eqid 
 |-  ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
28 21 22 24 25 26 27 14 imasmulval 
 |-  ( ( ph /\ { <. (/) , A >. , <. 1o , B >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ { <. (/) , C >. , <. 1o , D >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) .xb ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( { <. (/) , A >. , <. 1o , B >. } ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) ) )
29 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
30 fvexd 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> ( Scalar ` R ) e. _V )
31 2on 
 |-  2o e. On
32 31 a1i 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> 2o e. On )
33 simp1 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
34 simp2 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
35 simp3 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
36 16 29 30 32 33 34 35 27 prdsmulrval 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) -> ( { <. (/) , A >. , <. 1o , B >. } ( .r ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) = ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( .r ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 28 36 xpsaddlem 
 |-  ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )