Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . 4
โข
(Baseโ๐) =
(Baseโ๐) |
2 | | eqid 2726 |
. . . 4
โข
(ยท๐โ๐) =
(ยท๐โ๐) |
3 | | phssip.p |
. . . 4
โข ๐ =
(ยทifโ๐) |
4 | 1, 2, 3 | ipffval 21537 |
. . 3
โข ๐ = (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) |
5 | | phllmod 21519 |
. . . . . . 7
โข (๐ โ PreHil โ ๐ โ LMod) |
6 | | phssip.s |
. . . . . . . 8
โข ๐ = (LSubSpโ๐) |
7 | 6 | lsssubg 20802 |
. . . . . . 7
โข ((๐ โ LMod โง ๐ โ ๐) โ ๐ โ (SubGrpโ๐)) |
8 | 5, 7 | sylan 579 |
. . . . . 6
โข ((๐ โ PreHil โง ๐ โ ๐) โ ๐ โ (SubGrpโ๐)) |
9 | | phssip.x |
. . . . . . 7
โข ๐ = (๐ โพs ๐) |
10 | 9 | subgbas 19055 |
. . . . . 6
โข (๐ โ (SubGrpโ๐) โ ๐ = (Baseโ๐)) |
11 | 8, 10 | syl 17 |
. . . . 5
โข ((๐ โ PreHil โง ๐ โ ๐) โ ๐ = (Baseโ๐)) |
12 | | eqidd 2727 |
. . . . 5
โข ((๐ โ PreHil โง ๐ โ ๐) โ (๐ฅ(ยท๐โ๐)๐ฆ) = (๐ฅ(ยท๐โ๐)๐ฆ)) |
13 | 11, 11, 12 | mpoeq123dv 7479 |
. . . 4
โข ((๐ โ PreHil โง ๐ โ ๐) โ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) = (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
14 | | eqid 2726 |
. . . . . . 7
โข
(Baseโ๐) =
(Baseโ๐) |
15 | 14 | subgss 19052 |
. . . . . 6
โข (๐ โ (SubGrpโ๐) โ ๐ โ (Baseโ๐)) |
16 | 8, 15 | syl 17 |
. . . . 5
โข ((๐ โ PreHil โง ๐ โ ๐) โ ๐ โ (Baseโ๐)) |
17 | | resmpo 7523 |
. . . . 5
โข ((๐ โ (Baseโ๐) โง ๐ โ (Baseโ๐)) โ ((๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) โพ (๐ ร ๐)) = (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
18 | 16, 16, 17 | syl2anc 583 |
. . . 4
โข ((๐ โ PreHil โง ๐ โ ๐) โ ((๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) โพ (๐ ร ๐)) = (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
19 | | eqid 2726 |
. . . . . . . 8
โข
(ยท๐โ๐) =
(ยท๐โ๐) |
20 | 9, 19, 2 | ssipeq 21545 |
. . . . . . 7
โข (๐ โ ๐ โ
(ยท๐โ๐) =
(ยท๐โ๐)) |
21 | 20 | adantl 481 |
. . . . . 6
โข ((๐ โ PreHil โง ๐ โ ๐) โ
(ยท๐โ๐) =
(ยท๐โ๐)) |
22 | 21 | oveqd 7421 |
. . . . 5
โข ((๐ โ PreHil โง ๐ โ ๐) โ (๐ฅ(ยท๐โ๐)๐ฆ) = (๐ฅ(ยท๐โ๐)๐ฆ)) |
23 | 22 | mpoeq3dv 7483 |
. . . 4
โข ((๐ โ PreHil โง ๐ โ ๐) โ (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) = (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
24 | 13, 18, 23 | 3eqtr4rd 2777 |
. . 3
โข ((๐ โ PreHil โง ๐ โ ๐) โ (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) = ((๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) โพ (๐ ร ๐))) |
25 | 4, 24 | eqtrid 2778 |
. 2
โข ((๐ โ PreHil โง ๐ โ ๐) โ ๐ = ((๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) โพ (๐ ร ๐))) |
26 | | phssip.i |
. . . . 5
โข ยท =
(ยทifโ๐) |
27 | 14, 19, 26 | ipffval 21537 |
. . . 4
โข ยท =
(๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) |
28 | 27 | a1i 11 |
. . 3
โข ((๐ โ PreHil โง ๐ โ ๐) โ ยท = (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
29 | 28 | reseq1d 5973 |
. 2
โข ((๐ โ PreHil โง ๐ โ ๐) โ ( ยท โพ (๐ ร ๐)) = ((๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) โพ (๐ ร ๐))) |
30 | 25, 29 | eqtr4d 2769 |
1
โข ((๐ โ PreHil โง ๐ โ ๐) โ ๐ = ( ยท โพ (๐ ร ๐))) |