Step | Hyp | Ref
| Expression |
1 | | eqidd 2733 |
. . . . . 6
β’ (π β ((π½ Ξ©1 π) /s (
βphβπ½)) = ((π½ Ξ©1 π) /s (
βphβπ½))) |
2 | | eqidd 2733 |
. . . . . 6
β’ (π β (Baseβ(π½ Ξ©1 π)) = (Baseβ(π½ Ξ©1 π))) |
3 | | fvexd 6906 |
. . . . . 6
β’ (π β (
βphβπ½) β V) |
4 | | ovexd 7446 |
. . . . . 6
β’ (π β (π½ Ξ©1 π) β V) |
5 | | elpi1.g |
. . . . . . . 8
β’ πΊ = (π½ Ο1 π) |
6 | | elpi1.1 |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
7 | | elpi1.2 |
. . . . . . . 8
β’ (π β π β π) |
8 | | eqid 2732 |
. . . . . . . 8
β’ (π½ Ξ©1 π) = (π½ Ξ©1 π) |
9 | | elpi1.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΊ) |
10 | 9 | a1i 11 |
. . . . . . . 8
β’ (π β π΅ = (BaseβπΊ)) |
11 | 5, 6, 7, 8, 10, 2 | pi1blem 24779 |
. . . . . . 7
β’ (π β (((
βphβπ½) β (Baseβ(π½ Ξ©1 π))) β (Baseβ(π½ Ξ©1 π)) β§ (Baseβ(π½ Ξ©1 π)) β (II Cn π½))) |
12 | 11 | simpld 495 |
. . . . . 6
β’ (π β ((
βphβπ½) β (Baseβ(π½ Ξ©1 π))) β (Baseβ(π½ Ξ©1 π))) |
13 | 1, 2, 3, 4, 12 | qusin 17494 |
. . . . 5
β’ (π β ((π½ Ξ©1 π) /s (
βphβπ½)) = ((π½ Ξ©1 π) /s ((
βphβπ½) β© ((Baseβ(π½ Ξ©1 π)) Γ (Baseβ(π½ Ξ©1 π)))))) |
14 | 5, 6, 7, 8 | pi1val 24777 |
. . . . 5
β’ (π β πΊ = ((π½ Ξ©1 π) /s (
βphβπ½))) |
15 | 5, 6, 7, 8, 10, 2 | pi1buni 24780 |
. . . . . . . 8
β’ (π β βͺ π΅ =
(Baseβ(π½
Ξ©1 π))) |
16 | 15 | sqxpeqd 5708 |
. . . . . . 7
β’ (π β (βͺ π΅
Γ βͺ π΅) = ((Baseβ(π½ Ξ©1 π)) Γ (Baseβ(π½ Ξ©1 π)))) |
17 | 16 | ineq2d 4212 |
. . . . . 6
β’ (π β ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))
= (( βphβπ½) β© ((Baseβ(π½ Ξ©1 π)) Γ (Baseβ(π½ Ξ©1 π))))) |
18 | 17 | oveq2d 7427 |
. . . . 5
β’ (π β ((π½ Ξ©1 π) /s ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))
= ((π½ Ξ©1
π) /s ((
βphβπ½) β© ((Baseβ(π½ Ξ©1 π)) Γ (Baseβ(π½ Ξ©1 π)))))) |
19 | 13, 14, 18 | 3eqtr4d 2782 |
. . . 4
β’ (π β πΊ = ((π½ Ξ©1 π) /s ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))) |
20 | | phtpcer 24735 |
. . . . . 6
β’ (
βphβπ½) Er (II Cn π½) |
21 | 20 | a1i 11 |
. . . . 5
β’ (π β (
βphβπ½) Er (II Cn π½)) |
22 | 11 | simprd 496 |
. . . . . 6
β’ (π β (Baseβ(π½ Ξ©1 π)) β (II Cn π½)) |
23 | 15, 22 | eqsstrd 4020 |
. . . . 5
β’ (π β βͺ π΅
β (II Cn π½)) |
24 | 21, 23 | erinxp 8787 |
. . . 4
β’ (π β ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))
Er βͺ π΅) |
25 | | eqid 2732 |
. . . . 5
β’ ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))
= (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)) |
26 | | eqid 2732 |
. . . . 5
β’
(+gβ(π½ Ξ©1 π)) = (+gβ(π½ Ξ©1 π)) |
27 | 5, 6, 7, 10, 25, 8, 26 | pi1cpbl 24784 |
. . . 4
β’ (π β ((π(( βphβπ½) β© (βͺ π΅
Γ βͺ π΅))π β§ π(( βphβπ½) β© (βͺ π΅
Γ βͺ π΅))π) β (π(+gβ(π½ Ξ©1 π))π)(( βphβπ½) β© (βͺ π΅
Γ βͺ π΅))(π(+gβ(π½ Ξ©1 π))π))) |
28 | 6 | adantr 481 |
. . . . . . 7
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β π½ β (TopOnβπ)) |
29 | 7 | adantr 481 |
. . . . . . 7
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β π β π) |
30 | 8, 28, 29 | om1plusg 24774 |
. . . . . 6
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β
(*πβπ½) = (+gβ(π½ Ξ©1 π))) |
31 | 30 | oveqd 7428 |
. . . . 5
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β (π(*πβπ½)π) = (π(+gβ(π½ Ξ©1 π))π)) |
32 | 15 | adantr 481 |
. . . . . 6
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β βͺ π΅ =
(Baseβ(π½
Ξ©1 π))) |
33 | | simprl 769 |
. . . . . 6
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β π β βͺ π΅) |
34 | | simprr 771 |
. . . . . 6
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β π β βͺ π΅) |
35 | 8, 28, 29, 32, 33, 34 | om1addcl 24773 |
. . . . 5
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β (π(*πβπ½)π) β βͺ π΅) |
36 | 31, 35 | eqeltrrd 2834 |
. . . 4
β’ ((π β§ (π β βͺ π΅ β§ π β βͺ π΅)) β (π(+gβ(π½ Ξ©1 π))π) β βͺ π΅) |
37 | | pi1addf.p |
. . . 4
β’ + =
(+gβπΊ) |
38 | 19, 15, 24, 4, 27, 36, 26, 37 | qusaddf 17504 |
. . 3
β’ (π β + :((βͺ π΅
/ (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))
Γ (βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))))βΆ(βͺ
π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))) |
39 | 5, 6, 7, 10, 25 | pi1bas3 24783 |
. . . . 5
β’ (π β π΅ = (βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))) |
40 | 39 | sqxpeqd 5708 |
. . . 4
β’ (π β (π΅ Γ π΅) = ((βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))
Γ (βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))))) |
41 | 40 | feq2d 6703 |
. . 3
β’ (π β ( + :(π΅ Γ π΅)βΆ(βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))
β +
:((βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))
Γ (βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))))βΆ(βͺ
π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))))) |
42 | 38, 41 | mpbird 256 |
. 2
β’ (π β + :(π΅ Γ π΅)βΆ(βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅)))) |
43 | 39 | feq3d 6704 |
. 2
β’ (π β ( + :(π΅ Γ π΅)βΆπ΅ β + :(π΅ Γ π΅)βΆ(βͺ π΅ / ((
βphβπ½) β© (βͺ π΅ Γ βͺ π΅))))) |
44 | 42, 43 | mpbird 256 |
1
β’ (π β + :(π΅ Γ π΅)βΆπ΅) |