Step | Hyp | Ref
| Expression |
1 | | basfn 12520 |
. . . . 5
β’ Base Fn
V |
2 | | vex 2741 |
. . . . 5
β’ π β V |
3 | | funfvex 5533 |
. . . . . 6
β’ ((Fun
Base β§ π β dom
Base) β (Baseβπ)
β V) |
4 | 3 | funfni 5317 |
. . . . 5
β’ ((Base Fn
V β§ π β V) β
(Baseβπ) β
V) |
5 | 1, 2, 4 | mp2an 426 |
. . . 4
β’
(Baseβπ)
β V |
6 | 5 | a1i 9 |
. . 3
β’ (π = π β (Baseβπ) β V) |
7 | | fveq2 5516 |
. . . 4
β’ (π = π β (Baseβπ) = (Baseβπ)) |
8 | | ismgm.b |
. . . 4
β’ π΅ = (Baseβπ) |
9 | 7, 8 | eqtr4di 2228 |
. . 3
β’ (π = π β (Baseβπ) = π΅) |
10 | | plusgslid 12571 |
. . . . . . 7
β’
(+g = Slot (+gβndx) β§
(+gβndx) β β) |
11 | 10 | slotex 12489 |
. . . . . 6
β’ (π β V β
(+gβπ)
β V) |
12 | 11 | elv 2742 |
. . . . 5
β’
(+gβπ) β V |
13 | 12 | a1i 9 |
. . . 4
β’ ((π = π β§ π = π΅) β (+gβπ) β V) |
14 | | fveq2 5516 |
. . . . . 6
β’ (π = π β (+gβπ) = (+gβπ)) |
15 | 14 | adantr 276 |
. . . . 5
β’ ((π = π β§ π = π΅) β (+gβπ) = (+gβπ)) |
16 | | ismgm.o |
. . . . 5
β’ β¬ =
(+gβπ) |
17 | 15, 16 | eqtr4di 2228 |
. . . 4
β’ ((π = π β§ π = π΅) β (+gβπ) = β¬ ) |
18 | | simplr 528 |
. . . . 5
β’ (((π = π β§ π = π΅) β§ π = β¬ ) β π = π΅) |
19 | | oveq 5881 |
. . . . . . . 8
β’ (π = β¬ β (π₯ππ¦) = (π₯ β¬ π¦)) |
20 | 19 | adantl 277 |
. . . . . . 7
β’ (((π = π β§ π = π΅) β§ π = β¬ ) β (π₯ππ¦) = (π₯ β¬ π¦)) |
21 | 20, 18 | eleq12d 2248 |
. . . . . 6
β’ (((π = π β§ π = π΅) β§ π = β¬ ) β ((π₯ππ¦) β π β (π₯ β¬ π¦) β π΅)) |
22 | 18, 21 | raleqbidv 2685 |
. . . . 5
β’ (((π = π β§ π = π΅) β§ π = β¬ ) β
(βπ¦ β π (π₯ππ¦) β π β βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |
23 | 18, 22 | raleqbidv 2685 |
. . . 4
β’ (((π = π β§ π = π΅) β§ π = β¬ ) β
(βπ₯ β π βπ¦ β π (π₯ππ¦) β π β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |
24 | 13, 17, 23 | sbcied2 3001 |
. . 3
β’ ((π = π β§ π = π΅) β ([(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |
25 | 6, 9, 24 | sbcied2 3001 |
. 2
β’ (π = π β ([(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |
26 | | df-mgm 12775 |
. 2
β’ Mgm =
{π β£
[(Baseβπ) /
π][(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π} |
27 | 25, 26 | elab2g 2885 |
1
β’ (π β π β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) |