Metamath Proof Explorer

Theorem mendval

Description: Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mendval.b 
|- B = ( M LMHom M )
mendval.p 
|- .+ = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )
mendval.t 
|- .X. = ( x e. B , y e. B |-> ( x o. y ) )
mendval.s 
|- S = ( Scalar ` M )
mendval.v 
|- .x. = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
Assertion mendval 
|- ( M e. X -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )

Proof

Step Hyp Ref Expression
1 mendval.b 
 |-  B = ( M LMHom M )
2 mendval.p 
 |-  .+ = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )
3 mendval.t 
 |-  .X. = ( x e. B , y e. B |-> ( x o. y ) )
4 mendval.s 
 |-  S = ( Scalar ` M )
5 mendval.v 
 |-  .x. = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
6 elex 
 |-  ( M e. X -> M e. _V )
7 oveq12 
 |-  ( ( m = M /\ m = M ) -> ( m LMHom m ) = ( M LMHom M ) )
8 7 anidms 
 |-  ( m = M -> ( m LMHom m ) = ( M LMHom M ) )
9 8 1 eqtr4di 
 |-  ( m = M -> ( m LMHom m ) = B )
10 9 csbeq1d 
 |-  ( m = M -> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) = [_ B / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
11 ovex 
 |-  ( m LMHom m ) e. _V
12 9 11 eqeltrrdi 
 |-  ( m = M -> B e. _V )
13 simpr 
 |-  ( ( m = M /\ b = B ) -> b = B )
14 13 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
15 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
16 15 ofeqd 
 |-  ( m = M -> oF ( +g ` m ) = oF ( +g ` M ) )
17 16 oveqdr 
 |-  ( ( m = M /\ b = B ) -> ( x oF ( +g ` m ) y ) = ( x oF ( +g ` M ) y ) )
18 13 13 17 mpoeq123dv 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) ) )
19 18 2 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) = .+ )
20 19 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. = <. ( +g ` ndx ) , .+ >. )
21 eqidd 
 |-  ( ( m = M /\ b = B ) -> ( x o. y ) = ( x o. y ) )
22 13 13 21 mpoeq123dv 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x o. y ) ) = ( x e. B , y e. B |-> ( x o. y ) ) )
23 22 3 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x o. y ) ) = .X. )
24 23 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. = <. ( .r ` ndx ) , .X. >. )
25 14 20 24 tpeq123d 
 |-  ( ( m = M /\ b = B ) -> { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } )
26 fveq2 
 |-  ( m = M -> ( Scalar ` m ) = ( Scalar ` M ) )
27 26 adantr 
 |-  ( ( m = M /\ b = B ) -> ( Scalar ` m ) = ( Scalar ` M ) )
28 27 4 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( Scalar ` m ) = S )
29 28 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( Scalar ` ndx ) , ( Scalar ` m ) >. = <. ( Scalar ` ndx ) , S >. )
30 28 fveq2d 
 |-  ( ( m = M /\ b = B ) -> ( Base ` ( Scalar ` m ) ) = ( Base ` S ) )
31 fveq2 
 |-  ( m = M -> ( .s ` m ) = ( .s ` M ) )
32 31 adantr 
 |-  ( ( m = M /\ b = B ) -> ( .s ` m ) = ( .s ` M ) )
33 32 ofeqd 
 |-  ( ( m = M /\ b = B ) -> oF ( .s ` m ) = oF ( .s ` M ) )
34 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
35 34 adantr 
 |-  ( ( m = M /\ b = B ) -> ( Base ` m ) = ( Base ` M ) )
36 35 xpeq1d 
 |-  ( ( m = M /\ b = B ) -> ( ( Base ` m ) X. { x } ) = ( ( Base ` M ) X. { x } ) )
37 eqidd 
 |-  ( ( m = M /\ b = B ) -> y = y )
38 33 36 37 oveq123d 
 |-  ( ( m = M /\ b = B ) -> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
39 30 13 38 mpoeq123dv 
 |-  ( ( m = M /\ b = B ) -> ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) )
40 39 5 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) = .x. )
41 40 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. = <. ( .s ` ndx ) , .x. >. )
42 29 41 preq12d 
 |-  ( ( m = M /\ b = B ) -> { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } = { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )
43 25 42 uneq12d 
 |-  ( ( m = M /\ b = B ) -> ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
44 12 43 csbied 
 |-  ( m = M -> [_ B / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
45 10 44 eqtrd 
 |-  ( m = M -> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
46 df-mend 
 |-  MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
47 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V
48 prex 
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } e. _V
49 47 48 unex 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) e. _V
50 45 46 49 fvmpt 
 |-  ( M e. _V -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
51 6 50 syl 
 |-  ( M e. X -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )