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 𝑠 I
pwsdiagmhm.b B = Base R
pwsdiagmhm.f F = x B I × x
Assertion pwsdiagmhm R Mnd I W F R MndHom Y

Proof

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