Step | Hyp | Ref
| Expression |
1 | | frlmphl.y |
. . . . . . 7
โข ๐ = (๐
freeLMod ๐ผ) |
2 | | frlmphl.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
3 | | frlmphl.v |
. . . . . . 7
โข ๐ = (Baseโ๐) |
4 | 1, 2, 3 | frlmbasmap 21314 |
. . . . . 6
โข ((๐ผ โ ๐ โง ๐น โ ๐) โ ๐น โ (๐ต โm ๐ผ)) |
5 | 4 | ad2ant2r 746 |
. . . . 5
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ ๐น โ (๐ต โm ๐ผ)) |
6 | | elmapi 8843 |
. . . . 5
โข (๐น โ (๐ต โm ๐ผ) โ ๐น:๐ผโถ๐ต) |
7 | | ffn 6718 |
. . . . 5
โข (๐น:๐ผโถ๐ต โ ๐น Fn ๐ผ) |
8 | 5, 6, 7 | 3syl 18 |
. . . 4
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ ๐น Fn ๐ผ) |
9 | 1, 2, 3 | frlmbasmap 21314 |
. . . . . 6
โข ((๐ผ โ ๐ โง ๐บ โ ๐) โ ๐บ โ (๐ต โm ๐ผ)) |
10 | 9 | ad2ant2rl 748 |
. . . . 5
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ ๐บ โ (๐ต โm ๐ผ)) |
11 | | elmapi 8843 |
. . . . 5
โข (๐บ โ (๐ต โm ๐ผ) โ ๐บ:๐ผโถ๐ต) |
12 | | ffn 6718 |
. . . . 5
โข (๐บ:๐ผโถ๐ต โ ๐บ Fn ๐ผ) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ ๐บ Fn ๐ผ) |
14 | | simpll 766 |
. . . 4
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ ๐ผ โ ๐) |
15 | | inidm 4219 |
. . . 4
โข (๐ผ โฉ ๐ผ) = ๐ผ |
16 | | eqidd 2734 |
. . . 4
โข ((((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โง ๐ฅ โ ๐ผ) โ (๐นโ๐ฅ) = (๐นโ๐ฅ)) |
17 | | eqidd 2734 |
. . . 4
โข ((((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โง ๐ฅ โ ๐ผ) โ (๐บโ๐ฅ) = (๐บโ๐ฅ)) |
18 | 8, 13, 14, 14, 15, 16, 17 | offval 7679 |
. . 3
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น โf ยท ๐บ) = (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ)))) |
19 | 18 | oveq2d 7425 |
. 2
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐
ฮฃg (๐น โf ยท ๐บ)) = (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ))))) |
20 | | ovexd 7444 |
. . 3
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ)))) โ V) |
21 | | fveq1 6891 |
. . . . . . 7
โข (๐ = ๐น โ (๐โ๐ฅ) = (๐นโ๐ฅ)) |
22 | 21 | oveq1d 7424 |
. . . . . 6
โข (๐ = ๐น โ ((๐โ๐ฅ) ยท (๐โ๐ฅ)) = ((๐นโ๐ฅ) ยท (๐โ๐ฅ))) |
23 | 22 | mpteq2dv 5251 |
. . . . 5
โข (๐ = ๐น โ (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))) = (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐โ๐ฅ)))) |
24 | 23 | oveq2d 7425 |
. . . 4
โข (๐ = ๐น โ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ)))) = (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐โ๐ฅ))))) |
25 | | fveq1 6891 |
. . . . . . 7
โข (๐ = ๐บ โ (๐โ๐ฅ) = (๐บโ๐ฅ)) |
26 | 25 | oveq2d 7425 |
. . . . . 6
โข (๐ = ๐บ โ ((๐นโ๐ฅ) ยท (๐โ๐ฅ)) = ((๐นโ๐ฅ) ยท (๐บโ๐ฅ))) |
27 | 26 | mpteq2dv 5251 |
. . . . 5
โข (๐ = ๐บ โ (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐โ๐ฅ))) = (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ)))) |
28 | 27 | oveq2d 7425 |
. . . 4
โข (๐ = ๐บ โ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐โ๐ฅ)))) = (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ))))) |
29 | | eqid 2733 |
. . . 4
โข (๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))))) = (๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))))) |
30 | 24, 28, 29 | ovmpog 7567 |
. . 3
โข ((๐น โ (๐ต โm ๐ผ) โง ๐บ โ (๐ต โm ๐ผ) โง (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ)))) โ V) โ (๐น(๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ)))))๐บ) = (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ))))) |
31 | 5, 10, 20, 30 | syl3anc 1372 |
. 2
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น(๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ)))))๐บ) = (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐นโ๐ฅ) ยท (๐บโ๐ฅ))))) |
32 | | frlmphl.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
33 | 1, 2, 32 | frlmip 21333 |
. . . . 5
โข ((๐ผ โ ๐ โง ๐
โ ๐) โ (๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))))) =
(ยท๐โ๐)) |
34 | 33 | adantr 482 |
. . . 4
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))))) =
(ยท๐โ๐)) |
35 | | frlmphl.j |
. . . 4
โข , =
(ยท๐โ๐) |
36 | 34, 35 | eqtr4di 2791 |
. . 3
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ))))) = , ) |
37 | 36 | oveqd 7426 |
. 2
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น(๐ โ (๐ต โm ๐ผ), ๐ โ (๐ต โm ๐ผ) โฆ (๐
ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ) ยท (๐โ๐ฅ)))))๐บ) = (๐น , ๐บ)) |
38 | 19, 31, 37 | 3eqtr2rd 2780 |
1
โข (((๐ผ โ ๐ โง ๐
โ ๐) โง (๐น โ ๐ โง ๐บ โ ๐)) โ (๐น , ๐บ) = (๐
ฮฃg (๐น โf ยท ๐บ))) |