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 𝑌 ) )