Metamath Proof Explorer

Theorem xpsaddlem

Description: Lemma for xpsadd and xpsmul . (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 )
xpsaddlem.m 
|- .x. = ( E ` R )
xpsaddlem.n 
|- .X. = ( E ` S )
xpsaddlem.p 
|- .xb = ( E ` T )
xpsaddlem.f 
|- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
xpsaddlem.u 
|- U = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
xpsaddlem.1 
|- ( ( ph /\ { <. (/) , A >. , <. 1o , B >. } e. ran F /\ { <. (/) , C >. , <. 1o , D >. } e. ran F ) -> ( ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) .xb ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( `' F ` ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) ) )
xpsaddlem.2 
|- ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` U ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` U ) ) -> ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) = ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) )
Assertion xpsaddlem 
|- ( 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 xpsaddlem.m 
 |-  .x. = ( E ` R )
13 xpsaddlem.n 
 |-  .X. = ( E ` S )
14 xpsaddlem.p 
 |-  .xb = ( E ` T )
15 xpsaddlem.f 
 |-  F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
16 xpsaddlem.u 
 |-  U = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
17 xpsaddlem.1 
 |-  ( ( ph /\ { <. (/) , A >. , <. 1o , B >. } e. ran F /\ { <. (/) , C >. , <. 1o , D >. } e. ran F ) -> ( ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) .xb ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( `' F ` ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) ) )
18 xpsaddlem.2 
 |-  ( ( { <. (/) , R >. , <. 1o , S >. } Fn 2o /\ { <. (/) , A >. , <. 1o , B >. } e. ( Base ` U ) /\ { <. (/) , C >. , <. 1o , D >. } e. ( Base ` U ) ) -> ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) = ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) )
19 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
20 15 xpsfval 
 |-  ( ( A e. X /\ B e. Y ) -> ( A F B ) = { <. (/) , A >. , <. 1o , B >. } )
21 6 7 20 syl2anc 
 |-  ( ph -> ( A F B ) = { <. (/) , A >. , <. 1o , B >. } )
22 19 21 eqtr3id 
 |-  ( ph -> ( F ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } )
23 6 7 opelxpd 
 |-  ( ph -> <. A , B >. e. ( X X. Y ) )
24 15 xpsff1o2 
 |-  F : ( X X. Y ) -1-1-onto-> ran F
25 f1of 
 |-  ( F : ( X X. Y ) -1-1-onto-> ran F -> F : ( X X. Y ) --> ran F )
26 24 25 ax-mp 
 |-  F : ( X X. Y ) --> ran F
27 26 ffvelrni 
 |-  ( <. A , B >. e. ( X X. Y ) -> ( F ` <. A , B >. ) e. ran F )
28 23 27 syl 
 |-  ( ph -> ( F ` <. A , B >. ) e. ran F )
29 22 28 eqeltrrd 
 |-  ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ran F )
30 df-ov 
 |-  ( C F D ) = ( F ` <. C , D >. )
31 15 xpsfval 
 |-  ( ( C e. X /\ D e. Y ) -> ( C F D ) = { <. (/) , C >. , <. 1o , D >. } )
32 8 9 31 syl2anc 
 |-  ( ph -> ( C F D ) = { <. (/) , C >. , <. 1o , D >. } )
33 30 32 eqtr3id 
 |-  ( ph -> ( F ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } )
34 8 9 opelxpd 
 |-  ( ph -> <. C , D >. e. ( X X. Y ) )
35 26 ffvelrni 
 |-  ( <. C , D >. e. ( X X. Y ) -> ( F ` <. C , D >. ) e. ran F )
36 34 35 syl 
 |-  ( ph -> ( F ` <. C , D >. ) e. ran F )
37 33 36 eqeltrrd 
 |-  ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ran F )
38 29 37 17 mpd3an23 
 |-  ( ph -> ( ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) .xb ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( `' F ` ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) ) )
39 f1ocnvfv 
 |-  ( ( F : ( X X. Y ) -1-1-onto-> ran F /\ <. A , B >. e. ( X X. Y ) ) -> ( ( F ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) )
40 24 23 39 sylancr 
 |-  ( ph -> ( ( F ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) )
41 22 40 mpd 
 |-  ( ph -> ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. )
42 f1ocnvfv 
 |-  ( ( F : ( X X. Y ) -1-1-onto-> ran F /\ <. C , D >. e. ( X X. Y ) ) -> ( ( F ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) )
43 24 34 42 sylancr 
 |-  ( ph -> ( ( F ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) )
44 33 43 mpd 
 |-  ( ph -> ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. )
45 41 44 oveq12d 
 |-  ( ph -> ( ( `' F ` { <. (/) , A >. , <. 1o , B >. } ) .xb ( `' F ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( <. A , B >. .xb <. C , D >. ) )
46 iftrue 
 |-  ( k = (/) -> if ( k = (/) , R , S ) = R )
47 46 fveq2d 
 |-  ( k = (/) -> ( E ` if ( k = (/) , R , S ) ) = ( E ` R ) )
48 47 12 eqtr4di 
 |-  ( k = (/) -> ( E ` if ( k = (/) , R , S ) ) = .x. )
49 iftrue 
 |-  ( k = (/) -> if ( k = (/) , A , B ) = A )
50 iftrue 
 |-  ( k = (/) -> if ( k = (/) , C , D ) = C )
51 48 49 50 oveq123d 
 |-  ( k = (/) -> ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) = ( A .x. C ) )
52 iftrue 
 |-  ( k = (/) -> if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) = ( A .x. C ) )
53 51 52 eqtr4d 
 |-  ( k = (/) -> ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) = if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) )
54 iffalse 
 |-  ( -. k = (/) -> if ( k = (/) , R , S ) = S )
55 54 fveq2d 
 |-  ( -. k = (/) -> ( E ` if ( k = (/) , R , S ) ) = ( E ` S ) )
56 55 13 eqtr4di 
 |-  ( -. k = (/) -> ( E ` if ( k = (/) , R , S ) ) = .X. )
57 iffalse 
 |-  ( -. k = (/) -> if ( k = (/) , A , B ) = B )
58 iffalse 
 |-  ( -. k = (/) -> if ( k = (/) , C , D ) = D )
59 56 57 58 oveq123d 
 |-  ( -. k = (/) -> ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) = ( B .X. D ) )
60 iffalse 
 |-  ( -. k = (/) -> if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) = ( B .X. D ) )
61 59 60 eqtr4d 
 |-  ( -. k = (/) -> ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) = if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) )
62 53 61 pm2.61i 
 |-  ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) = if ( k = (/) , ( A .x. C ) , ( B .X. D ) )
63 4 adantr 
 |-  ( ( ph /\ k e. 2o ) -> R e. V )
64 5 adantr 
 |-  ( ( ph /\ k e. 2o ) -> S e. W )
65 simpr 
 |-  ( ( ph /\ k e. 2o ) -> k e. 2o )
66 fvprif 
 |-  ( ( R e. V /\ S e. W /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
67 63 64 65 66 syl3anc 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
68 67 fveq2d 
 |-  ( ( ph /\ k e. 2o ) -> ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( E ` if ( k = (/) , R , S ) ) )
69 6 adantr 
 |-  ( ( ph /\ k e. 2o ) -> A e. X )
70 7 adantr 
 |-  ( ( ph /\ k e. 2o ) -> B e. Y )
71 fvprif 
 |-  ( ( A e. X /\ B e. Y /\ k e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = if ( k = (/) , A , B ) )
72 69 70 65 71 syl3anc 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = if ( k = (/) , A , B ) )
73 8 adantr 
 |-  ( ( ph /\ k e. 2o ) -> C e. X )
74 9 adantr 
 |-  ( ( ph /\ k e. 2o ) -> D e. Y )
75 fvprif 
 |-  ( ( C e. X /\ D e. Y /\ k e. 2o ) -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = if ( k = (/) , C , D ) )
76 73 74 65 75 syl3anc 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = if ( k = (/) , C , D ) )
77 68 72 76 oveq123d 
 |-  ( ( ph /\ k e. 2o ) -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) = ( if ( k = (/) , A , B ) ( E ` if ( k = (/) , R , S ) ) if ( k = (/) , C , D ) ) )
78 10 adantr 
 |-  ( ( ph /\ k e. 2o ) -> ( A .x. C ) e. X )
79 11 adantr 
 |-  ( ( ph /\ k e. 2o ) -> ( B .X. D ) e. Y )
80 fvprif 
 |-  ( ( ( A .x. C ) e. X /\ ( B .X. D ) e. Y /\ k e. 2o ) -> ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) = if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) )
81 78 79 65 80 syl3anc 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) = if ( k = (/) , ( A .x. C ) , ( B .X. D ) ) )
82 62 77 81 3eqtr4a 
 |-  ( ( ph /\ k e. 2o ) -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) = ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) )
83 82 mpteq2dva 
 |-  ( ph -> ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) = ( k e. 2o |-> ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) ) )
84 fnpr2o 
 |-  ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
85 4 5 84 syl2anc 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
86 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
87 1 2 3 4 5 15 86 16 xpsrnbas 
 |-  ( ph -> ran F = ( Base ` U ) )
88 29 87 eleqtrd 
 |-  ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ( Base ` U ) )
89 37 87 eleqtrd 
 |-  ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ( Base ` U ) )
90 85 88 89 18 syl3anc 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) = ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( E ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) )
91 fnpr2o 
 |-  ( ( ( A .x. C ) e. X /\ ( B .X. D ) e. Y ) -> { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } Fn 2o )
92 10 11 91 syl2anc 
 |-  ( ph -> { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } Fn 2o )
93 dffn5 
 |-  ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } Fn 2o <-> { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } = ( k e. 2o |-> ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) ) )
94 92 93 sylib 
 |-  ( ph -> { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } = ( k e. 2o |-> ( { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ` k ) ) )
95 83 90 94 3eqtr4d 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } )
96 95 fveq2d 
 |-  ( ph -> ( `' F ` ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) ) = ( `' F ` { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ) )
97 df-ov 
 |-  ( ( A .x. C ) F ( B .X. D ) ) = ( F ` <. ( A .x. C ) , ( B .X. D ) >. )
98 15 xpsfval 
 |-  ( ( ( A .x. C ) e. X /\ ( B .X. D ) e. Y ) -> ( ( A .x. C ) F ( B .X. D ) ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } )
99 10 11 98 syl2anc 
 |-  ( ph -> ( ( A .x. C ) F ( B .X. D ) ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } )
100 97 99 eqtr3id 
 |-  ( ph -> ( F ` <. ( A .x. C ) , ( B .X. D ) >. ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } )
101 10 11 opelxpd 
 |-  ( ph -> <. ( A .x. C ) , ( B .X. D ) >. e. ( X X. Y ) )
102 f1ocnvfv 
 |-  ( ( F : ( X X. Y ) -1-1-onto-> ran F /\ <. ( A .x. C ) , ( B .X. D ) >. e. ( X X. Y ) ) -> ( ( F ` <. ( A .x. C ) , ( B .X. D ) >. ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } -> ( `' F ` { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ) = <. ( A .x. C ) , ( B .X. D ) >. ) )
103 24 101 102 sylancr 
 |-  ( ph -> ( ( F ` <. ( A .x. C ) , ( B .X. D ) >. ) = { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } -> ( `' F ` { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ) = <. ( A .x. C ) , ( B .X. D ) >. ) )
104 100 103 mpd 
 |-  ( ph -> ( `' F ` { <. (/) , ( A .x. C ) >. , <. 1o , ( B .X. D ) >. } ) = <. ( A .x. C ) , ( B .X. D ) >. )
105 96 104 eqtrd 
 |-  ( ph -> ( `' F ` ( { <. (/) , A >. , <. 1o , B >. } ( E ` U ) { <. (/) , C >. , <. 1o , D >. } ) ) = <. ( A .x. C ) , ( B .X. D ) >. )
106 38 45 105 3eqtr3d 
 |-  ( ph -> ( <. A , B >. .xb <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )