Step | Hyp | Ref
| Expression |
1 | | nmpropd2.1 |
. . . 4
โข (๐ โ ๐ต = (Baseโ๐พ)) |
2 | | nmpropd2.2 |
. . . 4
โข (๐ โ ๐ต = (Baseโ๐ฟ)) |
3 | 1, 2 | eqtr3d 2775 |
. . 3
โข (๐ โ (Baseโ๐พ) = (Baseโ๐ฟ)) |
4 | | nmpropd2.5 |
. . . . . 6
โข (๐ โ ((distโ๐พ) โพ (๐ต ร ๐ต)) = ((distโ๐ฟ) โพ (๐ต ร ๐ต))) |
5 | 1 | sqxpeqd 5669 |
. . . . . . 7
โข (๐ โ (๐ต ร ๐ต) = ((Baseโ๐พ) ร (Baseโ๐พ))) |
6 | 5 | reseq2d 5941 |
. . . . . 6
โข (๐ โ ((distโ๐พ) โพ (๐ต ร ๐ต)) = ((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))) |
7 | 4, 6 | eqtr3d 2775 |
. . . . 5
โข (๐ โ ((distโ๐ฟ) โพ (๐ต ร ๐ต)) = ((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))) |
8 | 2 | sqxpeqd 5669 |
. . . . . 6
โข (๐ โ (๐ต ร ๐ต) = ((Baseโ๐ฟ) ร (Baseโ๐ฟ))) |
9 | 8 | reseq2d 5941 |
. . . . 5
โข (๐ โ ((distโ๐ฟ) โพ (๐ต ร ๐ต)) = ((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))) |
10 | 7, 9 | eqtr3d 2775 |
. . . 4
โข (๐ โ ((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ))) = ((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))) |
11 | | eqidd 2734 |
. . . 4
โข (๐ โ ๐ = ๐) |
12 | | nmpropd2.4 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) |
13 | 1, 2, 12 | grpidpropd 18525 |
. . . 4
โข (๐ โ (0gโ๐พ) = (0gโ๐ฟ)) |
14 | 10, 11, 13 | oveq123d 7382 |
. . 3
โข (๐ โ (๐((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))(0gโ๐พ)) = (๐((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))(0gโ๐ฟ))) |
15 | 3, 14 | mpteq12dv 5200 |
. 2
โข (๐ โ (๐ โ (Baseโ๐พ) โฆ (๐((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))(0gโ๐พ))) = (๐ โ (Baseโ๐ฟ) โฆ (๐((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))(0gโ๐ฟ)))) |
16 | | nmpropd2.3 |
. . 3
โข (๐ โ ๐พ โ Grp) |
17 | | eqid 2733 |
. . . 4
โข
(normโ๐พ) =
(normโ๐พ) |
18 | | eqid 2733 |
. . . 4
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
19 | | eqid 2733 |
. . . 4
โข
(0gโ๐พ) = (0gโ๐พ) |
20 | | eqid 2733 |
. . . 4
โข
(distโ๐พ) =
(distโ๐พ) |
21 | | eqid 2733 |
. . . 4
โข
((distโ๐พ)
โพ ((Baseโ๐พ)
ร (Baseโ๐พ))) =
((distโ๐พ) โพ
((Baseโ๐พ) ร
(Baseโ๐พ))) |
22 | 17, 18, 19, 20, 21 | nmfval2 23970 |
. . 3
โข (๐พ โ Grp โ
(normโ๐พ) = (๐ โ (Baseโ๐พ) โฆ (๐((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))(0gโ๐พ)))) |
23 | 16, 22 | syl 17 |
. 2
โข (๐ โ (normโ๐พ) = (๐ โ (Baseโ๐พ) โฆ (๐((distโ๐พ) โพ ((Baseโ๐พ) ร (Baseโ๐พ)))(0gโ๐พ)))) |
24 | 1, 2, 12 | grppropd 18773 |
. . . 4
โข (๐ โ (๐พ โ Grp โ ๐ฟ โ Grp)) |
25 | 16, 24 | mpbid 231 |
. . 3
โข (๐ โ ๐ฟ โ Grp) |
26 | | eqid 2733 |
. . . 4
โข
(normโ๐ฟ) =
(normโ๐ฟ) |
27 | | eqid 2733 |
. . . 4
โข
(Baseโ๐ฟ) =
(Baseโ๐ฟ) |
28 | | eqid 2733 |
. . . 4
โข
(0gโ๐ฟ) = (0gโ๐ฟ) |
29 | | eqid 2733 |
. . . 4
โข
(distโ๐ฟ) =
(distโ๐ฟ) |
30 | | eqid 2733 |
. . . 4
โข
((distโ๐ฟ)
โพ ((Baseโ๐ฟ)
ร (Baseโ๐ฟ))) =
((distโ๐ฟ) โพ
((Baseโ๐ฟ) ร
(Baseโ๐ฟ))) |
31 | 26, 27, 28, 29, 30 | nmfval2 23970 |
. . 3
โข (๐ฟ โ Grp โ
(normโ๐ฟ) = (๐ โ (Baseโ๐ฟ) โฆ (๐((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))(0gโ๐ฟ)))) |
32 | 25, 31 | syl 17 |
. 2
โข (๐ โ (normโ๐ฟ) = (๐ โ (Baseโ๐ฟ) โฆ (๐((distโ๐ฟ) โพ ((Baseโ๐ฟ) ร (Baseโ๐ฟ)))(0gโ๐ฟ)))) |
33 | 15, 23, 32 | 3eqtr4d 2783 |
1
โข (๐ โ (normโ๐พ) = (normโ๐ฟ)) |