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 ) >. )