Step |
Hyp |
Ref |
Expression |
1 |
|
prdspjmhm.y |
⊢ 𝑌 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdspjmhm.b |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
3 |
|
prdspjmhm.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
4 |
|
prdspjmhm.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑋 ) |
5 |
|
prdspjmhm.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd ) |
6 |
|
prdspjmhm.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝐼 ) |
7 |
1 3 4 5
|
prdsmndd |
⊢ ( 𝜑 → 𝑌 ∈ Mnd ) |
8 |
5 6
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑅 ‘ 𝐴 ) ∈ Mnd ) |
9 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ 𝑋 ) |
10 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 ) |
11 |
5
|
ffnd |
⊢ ( 𝜑 → 𝑅 Fn 𝐼 ) |
12 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Fn 𝐼 ) |
13 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
14 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝐼 ) |
15 |
1 2 9 10 12 13 14
|
prdsbasprj |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ‘ 𝐴 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) ) |
16 |
15
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) ) |
17 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑋 ) |
18 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 ) |
19 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 Fn 𝐼 ) |
20 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 ) |
21 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 ) |
22 |
|
eqid |
⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) |
23 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐼 ) |
24 |
1 2 17 18 19 20 21 22 23
|
prdsplusgfval |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝐴 ) = ( ( 𝑦 ‘ 𝐴 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( 𝑧 ‘ 𝐴 ) ) ) |
25 |
2 22
|
mndcl |
⊢ ( ( 𝑌 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ∈ 𝐵 ) |
26 |
25
|
3expb |
⊢ ( ( 𝑌 ∈ Mnd ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ∈ 𝐵 ) |
27 |
7 26
|
sylan |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ∈ 𝐵 ) |
28 |
|
fveq1 |
⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝐴 ) ) |
29 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) |
30 |
|
fvex |
⊢ ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝐴 ) ∈ V |
31 |
28 29 30
|
fvmpt |
⊢ ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝐴 ) ) |
32 |
27 31
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ‘ 𝐴 ) ) |
33 |
|
fveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ‘ 𝐴 ) = ( 𝑦 ‘ 𝐴 ) ) |
34 |
|
fvex |
⊢ ( 𝑦 ‘ 𝐴 ) ∈ V |
35 |
33 29 34
|
fvmpt |
⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) = ( 𝑦 ‘ 𝐴 ) ) |
36 |
|
fveq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ‘ 𝐴 ) = ( 𝑧 ‘ 𝐴 ) ) |
37 |
|
fvex |
⊢ ( 𝑧 ‘ 𝐴 ) ∈ V |
38 |
36 29 37
|
fvmpt |
⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) = ( 𝑧 ‘ 𝐴 ) ) |
39 |
35 38
|
oveqan12d |
⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝐴 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( 𝑧 ‘ 𝐴 ) ) ) |
40 |
39
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝐴 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( 𝑧 ‘ 𝐴 ) ) ) |
41 |
24 32 40
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) ) |
42 |
41
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) ) |
43 |
|
eqid |
⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 ) |
44 |
2 43
|
mndidcl |
⊢ ( 𝑌 ∈ Mnd → ( 0g ‘ 𝑌 ) ∈ 𝐵 ) |
45 |
|
fveq1 |
⊢ ( 𝑥 = ( 0g ‘ 𝑌 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 0g ‘ 𝑌 ) ‘ 𝐴 ) ) |
46 |
|
fvex |
⊢ ( ( 0g ‘ 𝑌 ) ‘ 𝐴 ) ∈ V |
47 |
45 29 46
|
fvmpt |
⊢ ( ( 0g ‘ 𝑌 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 0g ‘ 𝑌 ) ) = ( ( 0g ‘ 𝑌 ) ‘ 𝐴 ) ) |
48 |
7 44 47
|
3syl |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 0g ‘ 𝑌 ) ) = ( ( 0g ‘ 𝑌 ) ‘ 𝐴 ) ) |
49 |
1 3 4 5
|
prds0g |
⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) ) |
50 |
49
|
fveq1d |
⊢ ( 𝜑 → ( ( 0g ∘ 𝑅 ) ‘ 𝐴 ) = ( ( 0g ‘ 𝑌 ) ‘ 𝐴 ) ) |
51 |
|
fvco3 |
⊢ ( ( 𝑅 : 𝐼 ⟶ Mnd ∧ 𝐴 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝐴 ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) ) |
52 |
5 6 51
|
syl2anc |
⊢ ( 𝜑 → ( ( 0g ∘ 𝑅 ) ‘ 𝐴 ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) ) |
53 |
48 50 52
|
3eqtr2d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) ) |
54 |
16 42 53
|
3jca |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) ) ) |
55 |
|
eqid |
⊢ ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) = ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) |
56 |
|
eqid |
⊢ ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) = ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) |
57 |
|
eqid |
⊢ ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) |
58 |
2 55 22 56 43 57
|
ismhm |
⊢ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom ( 𝑅 ‘ 𝐴 ) ) ↔ ( ( 𝑌 ∈ Mnd ∧ ( 𝑅 ‘ 𝐴 ) ∈ Mnd ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) : 𝐵 ⟶ ( Base ‘ ( 𝑅 ‘ 𝐴 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑦 ( +g ‘ 𝑌 ) 𝑧 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝐴 ) ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 0g ‘ 𝑌 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝐴 ) ) ) ) ) |
59 |
7 8 54 58
|
syl21anbrc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom ( 𝑅 ‘ 𝐴 ) ) ) |