Step |
Hyp |
Ref |
Expression |
1 |
|
submefmnd.g |
⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
submefmnd.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
3 |
|
submefmnd.0 |
⊢ 0 = ( 0g ‘ 𝑀 ) |
4 |
|
submefmnd.c |
⊢ 𝐹 = ( Base ‘ 𝑆 ) |
5 |
1
|
efmndmnd |
⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd ) |
6 |
|
simpl1 |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝑆 ∈ Mnd ) |
7 |
5 6
|
anim12i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝑀 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ) |
8 |
|
simpl2 |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ⊆ 𝐵 ) |
9 |
|
simpl3 |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 0 ∈ 𝐹 ) |
10 |
|
simpr |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) |
11 |
|
resmpo |
⊢ ( ( 𝐹 ⊆ 𝐵 ∧ 𝐹 ⊆ 𝐵 ) → ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) |
12 |
11
|
anidms |
⊢ ( 𝐹 ⊆ 𝐵 → ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) |
13 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
14 |
1 2 13
|
efmndplusg |
⊢ ( +g ‘ 𝑀 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) |
15 |
14
|
eqcomi |
⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ 𝑀 ) |
16 |
15
|
reseq1i |
⊢ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) |
17 |
12 16
|
eqtr3di |
⊢ ( 𝐹 ⊆ 𝐵 → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) |
18 |
17
|
3ad2ant2 |
⊢ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) |
19 |
18
|
adantr |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) |
20 |
10 19
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) |
21 |
8 9 20
|
3jca |
⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) ) |
23 |
2 4 3
|
mndissubm |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( ( 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ∧ ( +g ‘ 𝑆 ) = ( ( +g ‘ 𝑀 ) ↾ ( 𝐹 × 𝐹 ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) ) |
24 |
7 22 23
|
sylc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) |
25 |
24
|
ex |
⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹 ) ∧ ( +g ‘ 𝑆 ) = ( 𝑓 ∈ 𝐹 , 𝑔 ∈ 𝐹 ↦ ( 𝑓 ∘ 𝑔 ) ) ) → 𝐹 ∈ ( SubMnd ‘ 𝑀 ) ) ) |