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 ofeq 
 |-  ( ( +g ` m ) = ( +g ` M ) -> oF ( +g ` m ) = oF ( +g ` M ) )
17 15 16 syl 
 |-  ( m = M -> oF ( +g ` m ) = oF ( +g ` M ) )
18 17 oveqdr 
 |-  ( ( m = M /\ b = B ) -> ( x oF ( +g ` m ) y ) = ( x oF ( +g ` M ) y ) )
19 13 13 18 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 ) ) )
20 19 2 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) = .+ )
21 20 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. = <. ( +g ` ndx ) , .+ >. )
22 eqidd 
 |-  ( ( m = M /\ b = B ) -> ( x o. y ) = ( x o. y ) )
23 13 13 22 mpoeq123dv 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x o. y ) ) = ( x e. B , y e. B |-> ( x o. y ) ) )
24 23 3 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. b , y e. b |-> ( x o. y ) ) = .X. )
25 24 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. = <. ( .r ` ndx ) , .X. >. )
26 14 21 25 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. >. } )
27 fveq2 
 |-  ( m = M -> ( Scalar ` m ) = ( Scalar ` M ) )
28 27 adantr 
 |-  ( ( m = M /\ b = B ) -> ( Scalar ` m ) = ( Scalar ` M ) )
29 28 4 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( Scalar ` m ) = S )
30 29 opeq2d 
 |-  ( ( m = M /\ b = B ) -> <. ( Scalar ` ndx ) , ( Scalar ` m ) >. = <. ( Scalar ` ndx ) , S >. )
31 29 fveq2d 
 |-  ( ( m = M /\ b = B ) -> ( Base ` ( Scalar ` m ) ) = ( Base ` S ) )
32 fveq2 
 |-  ( m = M -> ( .s ` m ) = ( .s ` M ) )
33 32 adantr 
 |-  ( ( m = M /\ b = B ) -> ( .s ` m ) = ( .s ` M ) )
34 ofeq 
 |-  ( ( .s ` m ) = ( .s ` M ) -> oF ( .s ` m ) = oF ( .s ` M ) )
35 33 34 syl 
 |-  ( ( m = M /\ b = B ) -> oF ( .s ` m ) = oF ( .s ` M ) )
36 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
37 36 adantr 
 |-  ( ( m = M /\ b = B ) -> ( Base ` m ) = ( Base ` M ) )
38 37 xpeq1d 
 |-  ( ( m = M /\ b = B ) -> ( ( Base ` m ) X. { x } ) = ( ( Base ` M ) X. { x } ) )
39 eqidd 
 |-  ( ( m = M /\ b = B ) -> y = y )
40 35 38 39 oveq123d 
 |-  ( ( m = M /\ b = B ) -> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
41 31 13 40 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 ) ) )
42 41 5 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) = .x. )
43 42 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. >. )
44 30 43 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. >. } )
45 26 44 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. >. } ) )
46 12 45 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. >. } ) )
47 10 46 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. >. } ) )
48 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 ) ) >. } ) )
49 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V
50 prex 
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } e. _V
51 49 50 unex 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) e. _V
52 47 48 51 fvmpt 
 |-  ( M e. _V -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
53 6 52 syl 
 |-  ( M e. X -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )