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