Metamath Proof Explorer

Theorem pwsdiagmhm

Description: Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015)

Ref Expression
Hypotheses pwsdiagmhm.y 
|- Y = ( R ^s I )
pwsdiagmhm.b 
|- B = ( Base ` R )
pwsdiagmhm.f 
|- F = ( x e. B |-> ( I X. { x } ) )
Assertion pwsdiagmhm 
|- ( ( R e. Mnd /\ I e. W ) -> F e. ( R MndHom Y ) )

Proof

Step Hyp Ref Expression
1 pwsdiagmhm.y 
 |-  Y = ( R ^s I )
2 pwsdiagmhm.b 
 |-  B = ( Base ` R )
3 pwsdiagmhm.f 
 |-  F = ( x e. B |-> ( I X. { x } ) )
4 simpl 
 |-  ( ( R e. Mnd /\ I e. W ) -> R e. Mnd )
5 1 pwsmnd 
 |-  ( ( R e. Mnd /\ I e. W ) -> Y e. Mnd )
6 2 fvexi 
 |-  B e. _V
7 3 fdiagfn 
 |-  ( ( B e. _V /\ I e. W ) -> F : B --> ( B ^m I ) )
8 6 7 mpan 
 |-  ( I e. W -> F : B --> ( B ^m I ) )
9 8 adantl 
 |-  ( ( R e. Mnd /\ I e. W ) -> F : B --> ( B ^m I ) )
10 1 2 pwsbas 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )
11 10 feq3d 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( F : B --> ( B ^m I ) <-> F : B --> ( Base ` Y ) ) )
12 9 11 mpbid 
 |-  ( ( R e. Mnd /\ I e. W ) -> F : B --> ( Base ` Y ) )
13 simplr 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> I e. W )
14 eqid 
 |-  ( +g ` R ) = ( +g ` R )
15 2 14 mndcl 
 |-  ( ( R e. Mnd /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )
16 15 3expb 
 |-  ( ( R e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
17 16 adantlr 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
18 3 fvdiagfn 
 |-  ( ( I e. W /\ ( a ( +g ` R ) b ) e. B ) -> ( F ` ( a ( +g ` R ) b ) ) = ( I X. { ( a ( +g ` R ) b ) } ) )
19 13 17 18 syl2anc 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( I X. { ( a ( +g ` R ) b ) } ) )
20 3 fvdiagfn 
 |-  ( ( I e. W /\ a e. B ) -> ( F ` a ) = ( I X. { a } ) )
21 3 fvdiagfn 
 |-  ( ( I e. W /\ b e. B ) -> ( F ` b ) = ( I X. { b } ) )
22 20 21 oveqan12d 
 |-  ( ( ( I e. W /\ a e. B ) /\ ( I e. W /\ b e. B ) ) -> ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) = ( ( I X. { a } ) ( +g ` Y ) ( I X. { b } ) ) )
23 22 anandis 
 |-  ( ( I e. W /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) = ( ( I X. { a } ) ( +g ` Y ) ( I X. { b } ) ) )
24 23 adantll 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) = ( ( I X. { a } ) ( +g ` Y ) ( I X. { b } ) ) )
25 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
26 simpll 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> R e. Mnd )
27 1 2 25 pwsdiagel 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ a e. B ) -> ( I X. { a } ) e. ( Base ` Y ) )
28 27 adantrr 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( I X. { a } ) e. ( Base ` Y ) )
29 1 2 25 pwsdiagel 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ b e. B ) -> ( I X. { b } ) e. ( Base ` Y ) )
30 29 adantrl 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( I X. { b } ) e. ( Base ` Y ) )
31 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
32 1 25 26 13 28 30 14 31 pwsplusgval 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( ( I X. { a } ) ( +g ` Y ) ( I X. { b } ) ) = ( ( I X. { a } ) oF ( +g ` R ) ( I X. { b } ) ) )
33 id 
 |-  ( I e. W -> I e. W )
34 vex 
 |-  a e. _V
35 34 a1i 
 |-  ( I e. W -> a e. _V )
36 vex 
 |-  b e. _V
37 36 a1i 
 |-  ( I e. W -> b e. _V )
38 33 35 37 ofc12 
 |-  ( I e. W -> ( ( I X. { a } ) oF ( +g ` R ) ( I X. { b } ) ) = ( I X. { ( a ( +g ` R ) b ) } ) )
39 38 ad2antlr 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( ( I X. { a } ) oF ( +g ` R ) ( I X. { b } ) ) = ( I X. { ( a ( +g ` R ) b ) } ) )
40 24 32 39 3eqtrd 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) = ( I X. { ( a ( +g ` R ) b ) } ) )
41 19 40 eqtr4d 
 |-  ( ( ( R e. Mnd /\ I e. W ) /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) )
42 41 ralrimivva 
 |-  ( ( R e. Mnd /\ I e. W ) -> A. a e. B A. b e. B ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) )
43 simpr 
 |-  ( ( R e. Mnd /\ I e. W ) -> I e. W )
44 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
45 2 44 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. B )
46 45 adantr 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( 0g ` R ) e. B )
47 3 fvdiagfn 
 |-  ( ( I e. W /\ ( 0g ` R ) e. B ) -> ( F ` ( 0g ` R ) ) = ( I X. { ( 0g ` R ) } ) )
48 43 46 47 syl2anc 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( F ` ( 0g ` R ) ) = ( I X. { ( 0g ` R ) } ) )
49 1 44 pws0g 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( I X. { ( 0g ` R ) } ) = ( 0g ` Y ) )
50 48 49 eqtrd 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( F ` ( 0g ` R ) ) = ( 0g ` Y ) )
51 12 42 50 3jca 
 |-  ( ( R e. Mnd /\ I e. W ) -> ( F : B --> ( Base ` Y ) /\ A. a e. B A. b e. B ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) /\ ( F ` ( 0g ` R ) ) = ( 0g ` Y ) ) )
52 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
53 2 25 14 31 44 52 ismhm 
 |-  ( F e. ( R MndHom Y ) <-> ( ( R e. Mnd /\ Y e. Mnd ) /\ ( F : B --> ( Base ` Y ) /\ A. a e. B A. b e. B ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` Y ) ( F ` b ) ) /\ ( F ` ( 0g ` R ) ) = ( 0g ` Y ) ) ) )
54 4 5 51 53 syl21anbrc 
 |-  ( ( R e. Mnd /\ I e. W ) -> F e. ( R MndHom Y ) )