Step | Hyp | Ref
| Expression |
1 | | ielefmnd.g |
. . . 4
β’ πΊ = (EndoFMndβπ΄) |
2 | 1 | efmndsgrp 18697 |
. . 3
β’ πΊ β Smgrp |
3 | 2 | a1i 11 |
. 2
β’ (π΄ β π β πΊ β Smgrp) |
4 | 1 | ielefmnd 18698 |
. . 3
β’ (π΄ β π β ( I βΎ π΄) β (BaseβπΊ)) |
5 | | oveq1 7365 |
. . . . . . 7
β’ (π = ( I βΎ π΄) β (π(+gβπΊ)π) = (( I βΎ π΄)(+gβπΊ)π)) |
6 | 5 | eqeq1d 2739 |
. . . . . 6
β’ (π = ( I βΎ π΄) β ((π(+gβπΊ)π) = π β (( I βΎ π΄)(+gβπΊ)π) = π)) |
7 | | oveq2 7366 |
. . . . . . 7
β’ (π = ( I βΎ π΄) β (π(+gβπΊ)π) = (π(+gβπΊ)( I βΎ π΄))) |
8 | 7 | eqeq1d 2739 |
. . . . . 6
β’ (π = ( I βΎ π΄) β ((π(+gβπΊ)π) = π β (π(+gβπΊ)( I βΎ π΄)) = π)) |
9 | 6, 8 | anbi12d 632 |
. . . . 5
β’ (π = ( I βΎ π΄) β (((π(+gβπΊ)π) = π β§ (π(+gβπΊ)π) = π) β ((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π))) |
10 | 9 | ralbidv 3175 |
. . . 4
β’ (π = ( I βΎ π΄) β (βπ β (BaseβπΊ)((π(+gβπΊ)π) = π β§ (π(+gβπΊ)π) = π) β βπ β (BaseβπΊ)((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π))) |
11 | 10 | adantl 483 |
. . 3
β’ ((π΄ β π β§ π = ( I βΎ π΄)) β (βπ β (BaseβπΊ)((π(+gβπΊ)π) = π β§ (π(+gβπΊ)π) = π) β βπ β (BaseβπΊ)((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π))) |
12 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
13 | 1, 12 | efmndbasf 18686 |
. . . . . . 7
β’ (π β (BaseβπΊ) β π:π΄βΆπ΄) |
14 | 13 | adantl 483 |
. . . . . 6
β’ ((π΄ β π β§ π β (BaseβπΊ)) β π:π΄βΆπ΄) |
15 | | fcoi2 6718 |
. . . . . . 7
β’ (π:π΄βΆπ΄ β (( I βΎ π΄) β π) = π) |
16 | | fcoi1 6717 |
. . . . . . 7
β’ (π:π΄βΆπ΄ β (π β ( I βΎ π΄)) = π) |
17 | 15, 16 | jca 513 |
. . . . . 6
β’ (π:π΄βΆπ΄ β ((( I βΎ π΄) β π) = π β§ (π β ( I βΎ π΄)) = π)) |
18 | 14, 17 | syl 17 |
. . . . 5
β’ ((π΄ β π β§ π β (BaseβπΊ)) β ((( I βΎ π΄) β π) = π β§ (π β ( I βΎ π΄)) = π)) |
19 | | eqid 2737 |
. . . . . . . . 9
β’
(+gβπΊ) = (+gβπΊ) |
20 | 1, 12, 19 | efmndov 18692 |
. . . . . . . 8
β’ ((( I
βΎ π΄) β
(BaseβπΊ) β§ π β (BaseβπΊ)) β (( I βΎ π΄)(+gβπΊ)π) = (( I βΎ π΄) β π)) |
21 | 4, 20 | sylan 581 |
. . . . . . 7
β’ ((π΄ β π β§ π β (BaseβπΊ)) β (( I βΎ π΄)(+gβπΊ)π) = (( I βΎ π΄) β π)) |
22 | 21 | eqeq1d 2739 |
. . . . . 6
β’ ((π΄ β π β§ π β (BaseβπΊ)) β ((( I βΎ π΄)(+gβπΊ)π) = π β (( I βΎ π΄) β π) = π)) |
23 | 4 | anim1ci 617 |
. . . . . . . 8
β’ ((π΄ β π β§ π β (BaseβπΊ)) β (π β (BaseβπΊ) β§ ( I βΎ π΄) β (BaseβπΊ))) |
24 | 1, 12, 19 | efmndov 18692 |
. . . . . . . 8
β’ ((π β (BaseβπΊ) β§ ( I βΎ π΄) β (BaseβπΊ)) β (π(+gβπΊ)( I βΎ π΄)) = (π β ( I βΎ π΄))) |
25 | 23, 24 | syl 17 |
. . . . . . 7
β’ ((π΄ β π β§ π β (BaseβπΊ)) β (π(+gβπΊ)( I βΎ π΄)) = (π β ( I βΎ π΄))) |
26 | 25 | eqeq1d 2739 |
. . . . . 6
β’ ((π΄ β π β§ π β (BaseβπΊ)) β ((π(+gβπΊ)( I βΎ π΄)) = π β (π β ( I βΎ π΄)) = π)) |
27 | 22, 26 | anbi12d 632 |
. . . . 5
β’ ((π΄ β π β§ π β (BaseβπΊ)) β (((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π) β ((( I βΎ π΄) β π) = π β§ (π β ( I βΎ π΄)) = π))) |
28 | 18, 27 | mpbird 257 |
. . . 4
β’ ((π΄ β π β§ π β (BaseβπΊ)) β ((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π)) |
29 | 28 | ralrimiva 3144 |
. . 3
β’ (π΄ β π β βπ β (BaseβπΊ)((( I βΎ π΄)(+gβπΊ)π) = π β§ (π(+gβπΊ)( I βΎ π΄)) = π)) |
30 | 4, 11, 29 | rspcedvd 3584 |
. 2
β’ (π΄ β π β βπ β (BaseβπΊ)βπ β (BaseβπΊ)((π(+gβπΊ)π) = π β§ (π(+gβπΊ)π) = π)) |
31 | 12, 19 | ismnddef 18559 |
. 2
β’ (πΊ β Mnd β (πΊ β Smgrp β§ βπ β (BaseβπΊ)βπ β (BaseβπΊ)((π(+gβπΊ)π) = π β§ (π(+gβπΊ)π) = π))) |
32 | 3, 30, 31 | sylanbrc 584 |
1
β’ (π΄ β π β πΊ β Mnd) |