This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwsdiaglmhm

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

Ref Expression
Hypotheses pwsdiaglmhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsdiaglmhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pwsdiaglmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
Assertion pwsdiaglmhm ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 LMHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pwsdiaglmhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsdiaglmhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 pwsdiaglmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
4 eqid ⊢ ( ·𝑠 ‘ 𝑅 ) = ( ·𝑠 ‘ 𝑅 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
6 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
7 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
8 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
9 simpl ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ LMod )
10 1 pwslmod ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝑌 ∈ LMod )
11 1 6 pwssca ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑌 ) )
12 11 eqcomd ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑅 ) )
13 lmodgrp ⊢ ( 𝑅 ∈ LMod → 𝑅 ∈ Grp )
14 1 2 3 pwsdiagghm ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )
15 13 14 sylan ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )
16 simplr ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑊 )
17 2 6 4 8 lmodvscl ⊢ ( ( 𝑅 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
18 17 3expb ⊢ ( ( 𝑅 ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
19 18 adantlr ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
20 3 fvdiagfn ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) } ) )
21 16 19 20 syl2anc ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) } ) )
22 3 fvdiagfn ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐼 × { 𝑏 } ) )
23 22 ad2ant2l ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐼 × { 𝑏 } ) )
24 23 oveq2d ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝐼 × { 𝑏 } ) ) )
25 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
26 simpll ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ LMod )
27 simprl ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) )
28 1 2 25 pwsdiagel ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐼 × { 𝑏 } ) ∈ ( Base ‘ 𝑌 ) )
29 28 adantrl ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐼 × { 𝑏 } ) ∈ ( Base ‘ 𝑌 ) )
30 1 25 4 5 6 8 26 16 27 29 pwsvscafval ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝐼 × { 𝑏 } ) ) = ( ( 𝐼 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑅 ) ( 𝐼 × { 𝑏 } ) ) )
31 id ⊢ ( 𝐼 ∈ 𝑊 → 𝐼 ∈ 𝑊 )
32 vex ⊢ 𝑎 ∈ V
33 32 a1i ⊢ ( 𝐼 ∈ 𝑊 → 𝑎 ∈ V )
34 vex ⊢ 𝑏 ∈ V
35 34 a1i ⊢ ( 𝐼 ∈ 𝑊 → 𝑏 ∈ V )
36 31 33 35 ofc12 ⊢ ( 𝐼 ∈ 𝑊 → ( ( 𝐼 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑅 ) ( 𝐼 × { 𝑏 } ) ) = ( 𝐼 × { ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) } ) )
37 36 ad2antlr ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐼 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑅 ) ( 𝐼 × { 𝑏 } ) ) = ( 𝐼 × { ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) } ) )
38 24 30 37 3eqtrd ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝐼 × { ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) } ) )
39 21 38 eqtr4d ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝐹 ‘ 𝑏 ) ) )
40 2 4 5 6 7 8 9 10 12 15 39 islmhmd ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 LMHom 𝑌 ) )