Metamath Proof Explorer


Theorem xpsvsca

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

Ref Expression
Hypotheses xpssca.t
|- T = ( R Xs. S )
xpssca.g
|- G = ( Scalar ` R )
xpssca.1
|- ( ph -> R e. V )
xpssca.2
|- ( ph -> S e. W )
xpsvsca.x
|- X = ( Base ` R )
xpsvsca.y
|- Y = ( Base ` S )
xpsvsca.k
|- K = ( Base ` G )
xpsvsca.m
|- .x. = ( .s ` R )
xpsvsca.n
|- .X. = ( .s ` S )
xpsvsca.p
|- .xb = ( .s ` T )
xpsvsca.3
|- ( ph -> A e. K )
xpsvsca.4
|- ( ph -> B e. X )
xpsvsca.5
|- ( ph -> C e. Y )
xpsvsca.6
|- ( ph -> ( A .x. B ) e. X )
xpsvsca.7
|- ( ph -> ( A .X. C ) e. Y )
Assertion xpsvsca
|- ( ph -> ( A .xb <. B , C >. ) = <. ( A .x. B ) , ( A .X. C ) >. )

Proof

Step Hyp Ref Expression
1 xpssca.t
 |-  T = ( R Xs. S )
2 xpssca.g
 |-  G = ( Scalar ` R )
3 xpssca.1
 |-  ( ph -> R e. V )
4 xpssca.2
 |-  ( ph -> S e. W )
5 xpsvsca.x
 |-  X = ( Base ` R )
6 xpsvsca.y
 |-  Y = ( Base ` S )
7 xpsvsca.k
 |-  K = ( Base ` G )
8 xpsvsca.m
 |-  .x. = ( .s ` R )
9 xpsvsca.n
 |-  .X. = ( .s ` S )
10 xpsvsca.p
 |-  .xb = ( .s ` T )
11 xpsvsca.3
 |-  ( ph -> A e. K )
12 xpsvsca.4
 |-  ( ph -> B e. X )
13 xpsvsca.5
 |-  ( ph -> C e. Y )
14 xpsvsca.6
 |-  ( ph -> ( A .x. B ) e. X )
15 xpsvsca.7
 |-  ( ph -> ( A .X. C ) e. Y )
16 df-ov
 |-  ( B ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. )
17 eqid
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
18 17 xpsfval
 |-  ( ( B e. X /\ C e. Y ) -> ( B ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C ) = { <. (/) , B >. , <. 1o , C >. } )
19 12 13 18 syl2anc
 |-  ( ph -> ( B ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C ) = { <. (/) , B >. , <. 1o , C >. } )
20 16 19 eqtr3id
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. ) = { <. (/) , B >. , <. 1o , C >. } )
21 12 13 opelxpd
 |-  ( ph -> <. B , C >. e. ( X X. Y ) )
22 17 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 >. } )
23 f1of
 |-  ( ( 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 >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
24 22 23 ax-mp
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
25 24 ffvelrni
 |-  ( <. B , C >. e. ( X X. Y ) -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
26 21 25 syl
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
27 20 26 eqeltrrd
 |-  ( ph -> { <. (/) , B >. , <. 1o , C >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
28 eqid
 |-  ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( G Xs_ { <. (/) , R >. , <. 1o , S >. } )
29 1 5 6 3 4 17 2 28 xpsval
 |-  ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
30 1 5 6 3 4 17 2 28 xpsrnbas
 |-  ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
31 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 ) )
32 22 31 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 ) )
33 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 ) )
34 32 33 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 ) )
35 ovexd
 |-  ( ph -> ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
36 2 fvexi
 |-  G e. _V
37 36 a1i
 |-  ( T. -> G e. _V )
38 prex
 |-  { <. (/) , R >. , <. 1o , S >. } e. _V
39 38 a1i
 |-  ( T. -> { <. (/) , R >. , <. 1o , S >. } e. _V )
40 28 37 39 prdssca
 |-  ( T. -> G = ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
41 40 mptru
 |-  G = ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
42 eqid
 |-  ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
43 32 f1ovscpbl
 |-  ( ( ph /\ ( a e. K /\ b e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ c e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` b ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` c ) -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( a ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) b ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( a ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) c ) ) ) )
44 29 30 34 35 41 7 42 10 43 imasvscaval
 |-  ( ( ph /\ A e. K /\ { <. (/) , B >. , <. 1o , C >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( A .xb ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) ) )
45 11 27 44 mpd3an23
 |-  ( ph -> ( A .xb ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) ) )
46 f1ocnvfv
 |-  ( ( ( 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 >. } ) /\ <. B , C >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. ) = { <. (/) , B >. , <. 1o , C >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) = <. B , C >. ) )
47 22 21 46 sylancr
 |-  ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. B , C >. ) = { <. (/) , B >. , <. 1o , C >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) = <. B , C >. ) )
48 20 47 mpd
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) = <. B , C >. )
49 48 oveq2d
 |-  ( ph -> ( A .xb ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , B >. , <. 1o , C >. } ) ) = ( A .xb <. B , C >. ) )
50 iftrue
 |-  ( k = (/) -> if ( k = (/) , R , S ) = R )
51 50 fveq2d
 |-  ( k = (/) -> ( .s ` if ( k = (/) , R , S ) ) = ( .s ` R ) )
52 51 8 eqtr4di
 |-  ( k = (/) -> ( .s ` if ( k = (/) , R , S ) ) = .x. )
53 eqidd
 |-  ( k = (/) -> A = A )
54 iftrue
 |-  ( k = (/) -> if ( k = (/) , B , C ) = B )
55 52 53 54 oveq123d
 |-  ( k = (/) -> ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) = ( A .x. B ) )
56 iftrue
 |-  ( k = (/) -> if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) = ( A .x. B ) )
57 55 56 eqtr4d
 |-  ( k = (/) -> ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) = if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) )
58 iffalse
 |-  ( -. k = (/) -> if ( k = (/) , R , S ) = S )
59 58 fveq2d
 |-  ( -. k = (/) -> ( .s ` if ( k = (/) , R , S ) ) = ( .s ` S ) )
60 59 9 eqtr4di
 |-  ( -. k = (/) -> ( .s ` if ( k = (/) , R , S ) ) = .X. )
61 eqidd
 |-  ( -. k = (/) -> A = A )
62 iffalse
 |-  ( -. k = (/) -> if ( k = (/) , B , C ) = C )
63 60 61 62 oveq123d
 |-  ( -. k = (/) -> ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) = ( A .X. C ) )
64 iffalse
 |-  ( -. k = (/) -> if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) = ( A .X. C ) )
65 63 64 eqtr4d
 |-  ( -. k = (/) -> ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) = if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) )
66 57 65 pm2.61i
 |-  ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) = if ( k = (/) , ( A .x. B ) , ( A .X. C ) )
67 3 adantr
 |-  ( ( ph /\ k e. 2o ) -> R e. V )
68 4 adantr
 |-  ( ( ph /\ k e. 2o ) -> S e. W )
69 simpr
 |-  ( ( ph /\ k e. 2o ) -> k e. 2o )
70 fvprif
 |-  ( ( R e. V /\ S e. W /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
71 67 68 69 70 syl3anc
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
72 71 fveq2d
 |-  ( ( ph /\ k e. 2o ) -> ( .s ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( .s ` if ( k = (/) , R , S ) ) )
73 eqidd
 |-  ( ( ph /\ k e. 2o ) -> A = A )
74 12 adantr
 |-  ( ( ph /\ k e. 2o ) -> B e. X )
75 13 adantr
 |-  ( ( ph /\ k e. 2o ) -> C e. Y )
76 fvprif
 |-  ( ( B e. X /\ C e. Y /\ k e. 2o ) -> ( { <. (/) , B >. , <. 1o , C >. } ` k ) = if ( k = (/) , B , C ) )
77 74 75 69 76 syl3anc
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , B >. , <. 1o , C >. } ` k ) = if ( k = (/) , B , C ) )
78 72 73 77 oveq123d
 |-  ( ( ph /\ k e. 2o ) -> ( A ( .s ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , B >. , <. 1o , C >. } ` k ) ) = ( A ( .s ` if ( k = (/) , R , S ) ) if ( k = (/) , B , C ) ) )
79 14 adantr
 |-  ( ( ph /\ k e. 2o ) -> ( A .x. B ) e. X )
80 15 adantr
 |-  ( ( ph /\ k e. 2o ) -> ( A .X. C ) e. Y )
81 fvprif
 |-  ( ( ( A .x. B ) e. X /\ ( A .X. C ) e. Y /\ k e. 2o ) -> ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) = if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) )
82 79 80 69 81 syl3anc
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) = if ( k = (/) , ( A .x. B ) , ( A .X. C ) ) )
83 66 78 82 3eqtr4a
 |-  ( ( ph /\ k e. 2o ) -> ( A ( .s ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , B >. , <. 1o , C >. } ` k ) ) = ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) )
84 83 mpteq2dva
 |-  ( ph -> ( k e. 2o |-> ( A ( .s ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , B >. , <. 1o , C >. } ` k ) ) ) = ( k e. 2o |-> ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) ) )
85 eqid
 |-  ( Base ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
86 36 a1i
 |-  ( ph -> G e. _V )
87 2on
 |-  2o e. On
88 87 a1i
 |-  ( ph -> 2o e. On )
89 fnpr2o
 |-  ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
90 3 4 89 syl2anc
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
91 27 30 eleqtrd
 |-  ( ph -> { <. (/) , B >. , <. 1o , C >. } e. ( Base ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
92 28 85 42 7 86 88 90 11 91 prdsvscaval
 |-  ( ph -> ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) = ( k e. 2o |-> ( A ( .s ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , B >. , <. 1o , C >. } ` k ) ) ) )
93 fnpr2o
 |-  ( ( ( A .x. B ) e. X /\ ( A .X. C ) e. Y ) -> { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } Fn 2o )
94 14 15 93 syl2anc
 |-  ( ph -> { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } Fn 2o )
95 dffn5
 |-  ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } Fn 2o <-> { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } = ( k e. 2o |-> ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) ) )
96 94 95 sylib
 |-  ( ph -> { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } = ( k e. 2o |-> ( { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ` k ) ) )
97 84 92 96 3eqtr4d
 |-  ( ph -> ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } )
98 97 fveq2d
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ) )
99 df-ov
 |-  ( ( A .x. B ) ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ( A .X. C ) ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. ( A .x. B ) , ( A .X. C ) >. )
100 17 xpsfval
 |-  ( ( ( A .x. B ) e. X /\ ( A .X. C ) e. Y ) -> ( ( A .x. B ) ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ( A .X. C ) ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } )
101 14 15 100 syl2anc
 |-  ( ph -> ( ( A .x. B ) ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ( A .X. C ) ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } )
102 99 101 eqtr3id
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. ( A .x. B ) , ( A .X. C ) >. ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } )
103 14 15 opelxpd
 |-  ( ph -> <. ( A .x. B ) , ( A .X. C ) >. e. ( X X. Y ) )
104 f1ocnvfv
 |-  ( ( ( 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 >. } ) /\ <. ( A .x. B ) , ( A .X. C ) >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. ( A .x. B ) , ( A .X. C ) >. ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ) = <. ( A .x. B ) , ( A .X. C ) >. ) )
105 22 103 104 sylancr
 |-  ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. ( A .x. B ) , ( A .X. C ) >. ) = { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ) = <. ( A .x. B ) , ( A .X. C ) >. ) )
106 102 105 mpd
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , ( A .x. B ) >. , <. 1o , ( A .X. C ) >. } ) = <. ( A .x. B ) , ( A .X. C ) >. )
107 98 106 eqtrd
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` ( A ( .s ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , B >. , <. 1o , C >. } ) ) = <. ( A .x. B ) , ( A .X. C ) >. )
108 45 49 107 3eqtr3d
 |-  ( ph -> ( A .xb <. B , C >. ) = <. ( A .x. B ) , ( A .X. C ) >. )