Step | Hyp | Ref
| Expression |
1 | | anass 470 |
. 2
β’ (((π β (TopMnd β© LMod)
β§ πΉ β TopRing)
β§ Β· β ((πΎ Γt π½) Cn π½)) β (π β (TopMnd β© LMod) β§ (πΉ β TopRing β§ Β· β
((πΎ Γt
π½) Cn π½)))) |
2 | | df-3an 1090 |
. . . 4
β’ ((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β ((π β TopMnd β§ π β LMod) β§ πΉ β
TopRing)) |
3 | | elin 3927 |
. . . . 5
β’ (π β (TopMnd β© LMod)
β (π β TopMnd
β§ π β
LMod)) |
4 | 3 | anbi1i 625 |
. . . 4
β’ ((π β (TopMnd β© LMod)
β§ πΉ β TopRing)
β ((π β TopMnd
β§ π β LMod) β§
πΉ β
TopRing)) |
5 | 2, 4 | bitr4i 278 |
. . 3
β’ ((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β (π β (TopMnd β© LMod)
β§ πΉ β
TopRing)) |
6 | 5 | anbi1i 625 |
. 2
β’ (((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β§ Β· β
((πΎ Γt
π½) Cn π½)) β ((π β (TopMnd β© LMod) β§ πΉ β TopRing) β§ Β· β
((πΎ Γt
π½) Cn π½))) |
7 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π β (Scalarβπ€) = (Scalarβπ)) |
8 | | istlm.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (Scalarβπ€) = πΉ) |
10 | 9 | eleq1d 2819 |
. . . 4
β’ (π€ = π β ((Scalarβπ€) β TopRing β πΉ β TopRing)) |
11 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π β (
Β·sf βπ€) = ( Β·sf
βπ)) |
12 | | istlm.s |
. . . . . 6
β’ Β· = (
Β·sf βπ) |
13 | 11, 12 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (
Β·sf βπ€) = Β· ) |
14 | 9 | fveq2d 6847 |
. . . . . . . 8
β’ (π€ = π β (TopOpenβ(Scalarβπ€)) = (TopOpenβπΉ)) |
15 | | istlm.k |
. . . . . . . 8
β’ πΎ = (TopOpenβπΉ) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (TopOpenβ(Scalarβπ€)) = πΎ) |
17 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (TopOpenβπ€) = (TopOpenβπ)) |
18 | | istlm.j |
. . . . . . . 8
β’ π½ = (TopOpenβπ) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (TopOpenβπ€) = π½) |
20 | 16, 19 | oveq12d 7376 |
. . . . . 6
β’ (π€ = π β ((TopOpenβ(Scalarβπ€)) Γt
(TopOpenβπ€)) = (πΎ Γt π½)) |
21 | 20, 19 | oveq12d 7376 |
. . . . 5
β’ (π€ = π β (((TopOpenβ(Scalarβπ€)) Γt
(TopOpenβπ€)) Cn
(TopOpenβπ€)) =
((πΎ Γt
π½) Cn π½)) |
22 | 13, 21 | eleq12d 2828 |
. . . 4
β’ (π€ = π β ((
Β·sf βπ€) β (((TopOpenβ(Scalarβπ€)) Γt
(TopOpenβπ€)) Cn
(TopOpenβπ€)) β
Β·
β ((πΎ
Γt π½) Cn
π½))) |
23 | 10, 22 | anbi12d 632 |
. . 3
β’ (π€ = π β (((Scalarβπ€) β TopRing β§ (
Β·sf βπ€) β (((TopOpenβ(Scalarβπ€)) Γt
(TopOpenβπ€)) Cn
(TopOpenβπ€))) β
(πΉ β TopRing β§
Β·
β ((πΎ
Γt π½) Cn
π½)))) |
24 | | df-tlm 23529 |
. . 3
β’ TopMod =
{π€ β (TopMnd β©
LMod) β£ ((Scalarβπ€) β TopRing β§ (
Β·sf βπ€) β (((TopOpenβ(Scalarβπ€)) Γt
(TopOpenβπ€)) Cn
(TopOpenβπ€)))} |
25 | 23, 24 | elrab2 3649 |
. 2
β’ (π β TopMod β (π β (TopMnd β© LMod)
β§ (πΉ β TopRing
β§ Β· β ((πΎ Γt π½) Cn π½)))) |
26 | 1, 6, 25 | 3bitr4ri 304 |
1
β’ (π β TopMod β ((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β§ Β· β
((πΎ Γt
π½) Cn π½))) |