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