Step | Hyp | Ref
| Expression |
1 | | submefmnd.g |
. . . . 5
β’ π = (EndoFMndβπ΄) |
2 | 1 | efmndmnd 18770 |
. . . 4
β’ (π΄ β π β π β Mnd) |
3 | | simpl1 1192 |
. . . 4
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β π β Mnd) |
4 | 2, 3 | anim12i 614 |
. . 3
β’ ((π΄ β π β§ ((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π)))) β (π β Mnd β§ π β Mnd)) |
5 | | simpl2 1193 |
. . . . 5
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β πΉ β π΅) |
6 | | simpl3 1194 |
. . . . 5
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β 0 β πΉ) |
7 | | simpr 486 |
. . . . . 6
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) |
8 | | resmpo 7528 |
. . . . . . . . . 10
β’ ((πΉ β π΅ β§ πΉ β π΅) β ((π β π΅, π β π΅ β¦ (π β π)) βΎ (πΉ Γ πΉ)) = (π β πΉ, π β πΉ β¦ (π β π))) |
9 | 8 | anidms 568 |
. . . . . . . . 9
β’ (πΉ β π΅ β ((π β π΅, π β π΅ β¦ (π β π)) βΎ (πΉ Γ πΉ)) = (π β πΉ, π β πΉ β¦ (π β π))) |
10 | | submefmnd.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
11 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
12 | 1, 10, 11 | efmndplusg 18761 |
. . . . . . . . . . 11
β’
(+gβπ) = (π β π΅, π β π΅ β¦ (π β π)) |
13 | 12 | eqcomi 2742 |
. . . . . . . . . 10
β’ (π β π΅, π β π΅ β¦ (π β π)) = (+gβπ) |
14 | 13 | reseq1i 5978 |
. . . . . . . . 9
β’ ((π β π΅, π β π΅ β¦ (π β π)) βΎ (πΉ Γ πΉ)) = ((+gβπ) βΎ (πΉ Γ πΉ)) |
15 | 9, 14 | eqtr3di 2788 |
. . . . . . . 8
β’ (πΉ β π΅ β (π β πΉ, π β πΉ β¦ (π β π)) = ((+gβπ) βΎ (πΉ Γ πΉ))) |
16 | 15 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β (π β πΉ, π β πΉ β¦ (π β π)) = ((+gβπ) βΎ (πΉ Γ πΉ))) |
17 | 16 | adantr 482 |
. . . . . 6
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β (π β πΉ, π β πΉ β¦ (π β π)) = ((+gβπ) βΎ (πΉ Γ πΉ))) |
18 | 7, 17 | eqtrd 2773 |
. . . . 5
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β (+gβπ) = ((+gβπ) βΎ (πΉ Γ πΉ))) |
19 | 5, 6, 18 | 3jca 1129 |
. . . 4
β’ (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β (πΉ β π΅ β§ 0 β πΉ β§ (+gβπ) = ((+gβπ) βΎ (πΉ Γ πΉ)))) |
20 | 19 | adantl 483 |
. . 3
β’ ((π΄ β π β§ ((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π)))) β (πΉ β π΅ β§ 0 β πΉ β§ (+gβπ) = ((+gβπ) βΎ (πΉ Γ πΉ)))) |
21 | | submefmnd.c |
. . . 4
β’ πΉ = (Baseβπ) |
22 | | submefmnd.0 |
. . . 4
β’ 0 =
(0gβπ) |
23 | 10, 21, 22 | mndissubm 18688 |
. . 3
β’ ((π β Mnd β§ π β Mnd) β ((πΉ β π΅ β§ 0 β πΉ β§ (+gβπ) = ((+gβπ) βΎ (πΉ Γ πΉ))) β πΉ β (SubMndβπ))) |
24 | 4, 20, 23 | sylc 65 |
. 2
β’ ((π΄ β π β§ ((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π)))) β πΉ β (SubMndβπ)) |
25 | 24 | ex 414 |
1
β’ (π΄ β π β (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β πΉ β (SubMndβπ))) |