Step | Hyp | Ref
| Expression |
1 | | symgval.1 |
. 2
β’ πΊ = (SymGrpβπ΄) |
2 | | df-symg 19276 |
. . . . 5
β’ SymGrp =
(π₯ β V β¦
((EndoFMndβπ₯)
βΎs {β
β£ β:π₯β1-1-ontoβπ₯})) |
3 | 2 | a1i 11 |
. . . 4
β’ (π΄ β V β SymGrp = (π₯ β V β¦
((EndoFMndβπ₯)
βΎs {β
β£ β:π₯β1-1-ontoβπ₯}))) |
4 | | fveq2 6890 |
. . . . . 6
β’ (π₯ = π΄ β (EndoFMndβπ₯) = (EndoFMndβπ΄)) |
5 | | eqidd 2731 |
. . . . . . . . . 10
β’ (π₯ = π΄ β β = β) |
6 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = π΄ β π₯ = π΄) |
7 | 5, 6, 6 | f1oeq123d 6826 |
. . . . . . . . 9
β’ (π₯ = π΄ β (β:π₯β1-1-ontoβπ₯ β β:π΄β1-1-ontoβπ΄)) |
8 | 7 | abbidv 2799 |
. . . . . . . 8
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = {β β£ β:π΄β1-1-ontoβπ΄}) |
9 | | f1oeq1 6820 |
. . . . . . . . 9
β’ (β = π₯ β (β:π΄β1-1-ontoβπ΄ β π₯:π΄β1-1-ontoβπ΄)) |
10 | 9 | cbvabv 2803 |
. . . . . . . 8
β’ {β β£ β:π΄β1-1-ontoβπ΄} = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
11 | 8, 10 | eqtrdi 2786 |
. . . . . . 7
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = {π₯ β£ π₯:π΄β1-1-ontoβπ΄}) |
12 | | symgval.2 |
. . . . . . 7
β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
13 | 11, 12 | eqtr4di 2788 |
. . . . . 6
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = π΅) |
14 | 4, 13 | oveq12d 7429 |
. . . . 5
β’ (π₯ = π΄ β ((EndoFMndβπ₯) βΎs {β β£ β:π₯β1-1-ontoβπ₯}) = ((EndoFMndβπ΄) βΎs π΅)) |
15 | 14 | adantl 480 |
. . . 4
β’ ((π΄ β V β§ π₯ = π΄) β ((EndoFMndβπ₯) βΎs {β β£ β:π₯β1-1-ontoβπ₯}) = ((EndoFMndβπ΄) βΎs π΅)) |
16 | | id 22 |
. . . 4
β’ (π΄ β V β π΄ β V) |
17 | | ovexd 7446 |
. . . 4
β’ (π΄ β V β
((EndoFMndβπ΄)
βΎs π΅)
β V) |
18 | | nfv 1915 |
. . . 4
β’
β²π₯ π΄ β V |
19 | | nfcv 2901 |
. . . 4
β’
β²π₯π΄ |
20 | | nfcv 2901 |
. . . . 5
β’
β²π₯(EndoFMndβπ΄) |
21 | | nfcv 2901 |
. . . . 5
β’
β²π₯
βΎs |
22 | | nfab1 2903 |
. . . . . 6
β’
β²π₯{π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
23 | 12, 22 | nfcxfr 2899 |
. . . . 5
β’
β²π₯π΅ |
24 | 20, 21, 23 | nfov 7441 |
. . . 4
β’
β²π₯((EndoFMndβπ΄) βΎs π΅) |
25 | 3, 15, 16, 17, 18, 19, 24 | fvmptdf 7003 |
. . 3
β’ (π΄ β V β
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅)) |
26 | | ress0 17192 |
. . . . 5
β’ (β
βΎs π΅) =
β
|
27 | 26 | a1i 11 |
. . . 4
β’ (Β¬
π΄ β V β (β
βΎs π΅) =
β
) |
28 | | fvprc 6882 |
. . . . 5
β’ (Β¬
π΄ β V β
(EndoFMndβπ΄) =
β
) |
29 | 28 | oveq1d 7426 |
. . . 4
β’ (Β¬
π΄ β V β
((EndoFMndβπ΄)
βΎs π΅) =
(β
βΎs π΅)) |
30 | | fvprc 6882 |
. . . 4
β’ (Β¬
π΄ β V β
(SymGrpβπ΄) =
β
) |
31 | 27, 29, 30 | 3eqtr4rd 2781 |
. . 3
β’ (Β¬
π΄ β V β
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅)) |
32 | 25, 31 | pm2.61i 182 |
. 2
β’
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅) |
33 | 1, 32 | eqtri 2758 |
1
β’ πΊ = ((EndoFMndβπ΄) βΎs π΅) |