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