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 𝑌 = ( 𝑅s 𝐼 )
pwsdiagmhm.b 𝐵 = ( Base ‘ 𝑅 )
pwsdiagmhm.f 𝐹 = ( 𝑥𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
Assertion pwsdiagmhm ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pwsdiagmhm.y 𝑌 = ( 𝑅s 𝐼 )
2 pwsdiagmhm.b 𝐵 = ( Base ‘ 𝑅 )
3 pwsdiagmhm.f 𝐹 = ( 𝑥𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
4 simpl ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝑅 ∈ Mnd )
5 1 pwsmnd ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝑌 ∈ Mnd )
6 2 fvexi 𝐵 ∈ V
7 3 fdiagfn ( ( 𝐵 ∈ V ∧ 𝐼𝑊 ) → 𝐹 : 𝐵 ⟶ ( 𝐵m 𝐼 ) )
8 6 7 mpan ( 𝐼𝑊𝐹 : 𝐵 ⟶ ( 𝐵m 𝐼 ) )
9 8 adantl ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝐹 : 𝐵 ⟶ ( 𝐵m 𝐼 ) )
10 1 2 pwsbas ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐵m 𝐼 ) = ( Base ‘ 𝑌 ) )
11 10 feq3d ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐹 : 𝐵 ⟶ ( 𝐵m 𝐼 ) ↔ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑌 ) ) )
12 9 11 mpbid ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑌 ) )
13 simplr ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝐼𝑊 )
14 eqid ( +g𝑅 ) = ( +g𝑅 )
15 2 14 mndcl ( ( 𝑅 ∈ Mnd ∧ 𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 )
16 15 3expb ( ( 𝑅 ∈ Mnd ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 )
17 16 adantlr ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 )
18 3 fvdiagfn ( ( 𝐼𝑊 ∧ ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( +g𝑅 ) 𝑏 ) } ) )
19 13 17 18 syl2anc ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( +g𝑅 ) 𝑏 ) } ) )
20 3 fvdiagfn ( ( 𝐼𝑊𝑎𝐵 ) → ( 𝐹𝑎 ) = ( 𝐼 × { 𝑎 } ) )
21 3 fvdiagfn ( ( 𝐼𝑊𝑏𝐵 ) → ( 𝐹𝑏 ) = ( 𝐼 × { 𝑏 } ) )
22 20 21 oveqan12d ( ( ( 𝐼𝑊𝑎𝐵 ) ∧ ( 𝐼𝑊𝑏𝐵 ) ) → ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) = ( ( 𝐼 × { 𝑎 } ) ( +g𝑌 ) ( 𝐼 × { 𝑏 } ) ) )
23 22 anandis ( ( 𝐼𝑊 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) = ( ( 𝐼 × { 𝑎 } ) ( +g𝑌 ) ( 𝐼 × { 𝑏 } ) ) )
24 23 adantll ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) = ( ( 𝐼 × { 𝑎 } ) ( +g𝑌 ) ( 𝐼 × { 𝑏 } ) ) )
25 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
26 simpll ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑅 ∈ Mnd )
27 1 2 25 pwsdiagel ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ 𝑎𝐵 ) → ( 𝐼 × { 𝑎 } ) ∈ ( Base ‘ 𝑌 ) )
28 27 adantrr ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐼 × { 𝑎 } ) ∈ ( Base ‘ 𝑌 ) )
29 1 2 25 pwsdiagel ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ 𝑏𝐵 ) → ( 𝐼 × { 𝑏 } ) ∈ ( Base ‘ 𝑌 ) )
30 29 adantrl ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐼 × { 𝑏 } ) ∈ ( Base ‘ 𝑌 ) )
31 eqid ( +g𝑌 ) = ( +g𝑌 )
32 1 25 26 13 28 30 14 31 pwsplusgval ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝐼 × { 𝑎 } ) ( +g𝑌 ) ( 𝐼 × { 𝑏 } ) ) = ( ( 𝐼 × { 𝑎 } ) ∘f ( +g𝑅 ) ( 𝐼 × { 𝑏 } ) ) )
33 id ( 𝐼𝑊𝐼𝑊 )
34 vex 𝑎 ∈ V
35 34 a1i ( 𝐼𝑊𝑎 ∈ V )
36 vex 𝑏 ∈ V
37 36 a1i ( 𝐼𝑊𝑏 ∈ V )
38 33 35 37 ofc12 ( 𝐼𝑊 → ( ( 𝐼 × { 𝑎 } ) ∘f ( +g𝑅 ) ( 𝐼 × { 𝑏 } ) ) = ( 𝐼 × { ( 𝑎 ( +g𝑅 ) 𝑏 ) } ) )
39 38 ad2antlr ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝐼 × { 𝑎 } ) ∘f ( +g𝑅 ) ( 𝐼 × { 𝑏 } ) ) = ( 𝐼 × { ( 𝑎 ( +g𝑅 ) 𝑏 ) } ) )
40 24 32 39 3eqtrd ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( +g𝑅 ) 𝑏 ) } ) )
41 19 40 eqtr4d ( ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) )
42 41 ralrimivva ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ∀ 𝑎𝐵𝑏𝐵 ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) )
43 simpr ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝐼𝑊 )
44 eqid ( 0g𝑅 ) = ( 0g𝑅 )
45 2 44 mndidcl ( 𝑅 ∈ Mnd → ( 0g𝑅 ) ∈ 𝐵 )
46 45 adantr ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 0g𝑅 ) ∈ 𝐵 )
47 3 fvdiagfn ( ( 𝐼𝑊 ∧ ( 0g𝑅 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 𝐼 × { ( 0g𝑅 ) } ) )
48 43 46 47 syl2anc ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 𝐼 × { ( 0g𝑅 ) } ) )
49 1 44 pws0g ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐼 × { ( 0g𝑅 ) } ) = ( 0g𝑌 ) )
50 48 49 eqtrd ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 0g𝑌 ) )
51 12 42 50 3jca ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑎𝐵𝑏𝐵 ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) ∧ ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 0g𝑌 ) ) )
52 eqid ( 0g𝑌 ) = ( 0g𝑌 )
53 2 25 14 31 44 52 ismhm ( 𝐹 ∈ ( 𝑅 MndHom 𝑌 ) ↔ ( ( 𝑅 ∈ Mnd ∧ 𝑌 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑎𝐵𝑏𝐵 ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑌 ) ( 𝐹𝑏 ) ) ∧ ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 0g𝑌 ) ) ) )
54 4 5 51 53 syl21anbrc ( ( 𝑅 ∈ Mnd ∧ 𝐼𝑊 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑌 ) )