Step | Hyp | Ref
| Expression |
1 | | symgval.1 |
. 2
β’ πΊ = (SymGrpβπ΄) |
2 | | df-symg 19277 |
. . . . 5
β’ SymGrp =
(π₯ β V β¦
((EndoFMndβπ₯)
βΎs {β
β£ β:π₯β1-1-ontoβπ₯})) |
3 | 2 | a1i 11 |
. . . 4
β’ (π΄ β V β SymGrp = (π₯ β V β¦
((EndoFMndβπ₯)
βΎs {β
β£ β:π₯β1-1-ontoβπ₯}))) |
4 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = π΄ β (EndoFMndβπ₯) = (EndoFMndβπ΄)) |
5 | | eqidd 2732 |
. . . . . . . . . 10
β’ (π₯ = π΄ β β = β) |
6 | | id 22 |
. . . . . . . . . 10
β’ (π₯ = π΄ β π₯ = π΄) |
7 | 5, 6, 6 | f1oeq123d 6827 |
. . . . . . . . 9
β’ (π₯ = π΄ β (β:π₯β1-1-ontoβπ₯ β β:π΄β1-1-ontoβπ΄)) |
8 | 7 | abbidv 2800 |
. . . . . . . 8
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = {β β£ β:π΄β1-1-ontoβπ΄}) |
9 | | f1oeq1 6821 |
. . . . . . . . 9
β’ (β = π₯ β (β:π΄β1-1-ontoβπ΄ β π₯:π΄β1-1-ontoβπ΄)) |
10 | 9 | cbvabv 2804 |
. . . . . . . 8
β’ {β β£ β:π΄β1-1-ontoβπ΄} = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
11 | 8, 10 | eqtrdi 2787 |
. . . . . . 7
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = {π₯ β£ π₯:π΄β1-1-ontoβπ΄}) |
12 | | symgval.2 |
. . . . . . 7
β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
13 | 11, 12 | eqtr4di 2789 |
. . . . . 6
β’ (π₯ = π΄ β {β β£ β:π₯β1-1-ontoβπ₯} = π΅) |
14 | 4, 13 | oveq12d 7430 |
. . . . 5
β’ (π₯ = π΄ β ((EndoFMndβπ₯) βΎs {β β£ β:π₯β1-1-ontoβπ₯}) = ((EndoFMndβπ΄) βΎs π΅)) |
15 | 14 | adantl 481 |
. . . 4
β’ ((π΄ β V β§ π₯ = π΄) β ((EndoFMndβπ₯) βΎs {β β£ β:π₯β1-1-ontoβπ₯}) = ((EndoFMndβπ΄) βΎs π΅)) |
16 | | id 22 |
. . . 4
β’ (π΄ β V β π΄ β V) |
17 | | ovexd 7447 |
. . . 4
β’ (π΄ β V β
((EndoFMndβπ΄)
βΎs π΅)
β V) |
18 | | nfv 1916 |
. . . 4
β’
β²π₯ π΄ β V |
19 | | nfcv 2902 |
. . . 4
β’
β²π₯π΄ |
20 | | nfcv 2902 |
. . . . 5
β’
β²π₯(EndoFMndβπ΄) |
21 | | nfcv 2902 |
. . . . 5
β’
β²π₯
βΎs |
22 | | nfab1 2904 |
. . . . . 6
β’
β²π₯{π₯ β£ π₯:π΄β1-1-ontoβπ΄} |
23 | 12, 22 | nfcxfr 2900 |
. . . . 5
β’
β²π₯π΅ |
24 | 20, 21, 23 | nfov 7442 |
. . . 4
β’
β²π₯((EndoFMndβπ΄) βΎs π΅) |
25 | 3, 15, 16, 17, 18, 19, 24 | fvmptdf 7004 |
. . 3
β’ (π΄ β V β
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅)) |
26 | | ress0 17193 |
. . . . 5
β’ (β
βΎs π΅) =
β
|
27 | 26 | a1i 11 |
. . . 4
β’ (Β¬
π΄ β V β (β
βΎs π΅) =
β
) |
28 | | fvprc 6883 |
. . . . 5
β’ (Β¬
π΄ β V β
(EndoFMndβπ΄) =
β
) |
29 | 28 | oveq1d 7427 |
. . . 4
β’ (Β¬
π΄ β V β
((EndoFMndβπ΄)
βΎs π΅) =
(β
βΎs π΅)) |
30 | | fvprc 6883 |
. . . 4
β’ (Β¬
π΄ β V β
(SymGrpβπ΄) =
β
) |
31 | 27, 29, 30 | 3eqtr4rd 2782 |
. . 3
β’ (Β¬
π΄ β V β
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅)) |
32 | 25, 31 | pm2.61i 182 |
. 2
β’
(SymGrpβπ΄) =
((EndoFMndβπ΄)
βΎs π΅) |
33 | 1, 32 | eqtri 2759 |
1
β’ πΊ = ((EndoFMndβπ΄) βΎs π΅) |