Step | Hyp | Ref
| Expression |
1 | | pstmval.1 |
. . . . 5
β’ βΌ =
(~Metβπ·) |
2 | 1 | pstmval 32540 |
. . . 4
β’ (π· β (PsMetβπ) β (pstoMetβπ·) = (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)})) |
3 | 2 | 3ad2ant1 1134 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (pstoMetβπ·) = (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)})) |
4 | 3 | oveqd 7378 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ([π΄] βΌ
(pstoMetβπ·)[π΅] βΌ ) = ([π΄] βΌ (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)})[π΅] βΌ )) |
5 | 1 | fvexi 6860 |
. . . . 5
β’ βΌ β
V |
6 | 5 | ecelqsi 8718 |
. . . 4
β’ (π΄ β π β [π΄] βΌ β (π / βΌ )) |
7 | 6 | 3ad2ant2 1135 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β [π΄] βΌ β (π / βΌ )) |
8 | 5 | ecelqsi 8718 |
. . . 4
β’ (π΅ β π β [π΅] βΌ β (π / βΌ )) |
9 | 8 | 3ad2ant3 1136 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β [π΅] βΌ β (π / βΌ )) |
10 | | rexeq 3309 |
. . . . . 6
β’ (π₯ = [π΄] βΌ β
(βπ β π₯ βπ β π¦ π§ = (ππ·π) β βπ β [ π΄] βΌ βπ β π¦ π§ = (ππ·π))) |
11 | 10 | abbidv 2802 |
. . . . 5
β’ (π₯ = [π΄] βΌ β {π§ β£ βπ β π₯ βπ β π¦ π§ = (ππ·π)} = {π§ β£ βπ β [ π΄] βΌ βπ β π¦ π§ = (ππ·π)}) |
12 | 11 | unieqd 4883 |
. . . 4
β’ (π₯ = [π΄] βΌ β βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)} = βͺ {π§ β£ βπ β [ π΄] βΌ βπ β π¦ π§ = (ππ·π)}) |
13 | | rexeq 3309 |
. . . . . . 7
β’ (π¦ = [π΅] βΌ β
(βπ β π¦ π§ = (ππ·π) β βπ β [ π΅] βΌ π§ = (ππ·π))) |
14 | 13 | rexbidv 3172 |
. . . . . 6
β’ (π¦ = [π΅] βΌ β
(βπ β [ π΄] βΌ βπ β π¦ π§ = (ππ·π) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π))) |
15 | 14 | abbidv 2802 |
. . . . 5
β’ (π¦ = [π΅] βΌ β {π§ β£ βπ β [ π΄] βΌ βπ β π¦ π§ = (ππ·π)} = {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)}) |
16 | 15 | unieqd 4883 |
. . . 4
β’ (π¦ = [π΅] βΌ β βͺ {π§
β£ βπ β [
π΄] βΌ βπ β π¦ π§ = (ππ·π)} = βͺ {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)}) |
17 | | eqid 2733 |
. . . 4
β’ (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)}) = (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)}) |
18 | | ecexg 8658 |
. . . . . . 7
β’ ( βΌ β
V β [π΄] βΌ β
V) |
19 | 5, 18 | ax-mp 5 |
. . . . . 6
β’ [π΄] βΌ β
V |
20 | | ecexg 8658 |
. . . . . . 7
β’ ( βΌ β
V β [π΅] βΌ β
V) |
21 | 5, 20 | ax-mp 5 |
. . . . . 6
β’ [π΅] βΌ β
V |
22 | 19, 21 | ab2rexex 7916 |
. . . . 5
β’ {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} β V |
23 | 22 | uniex 7682 |
. . . 4
β’ βͺ {π§
β£ βπ β [
π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} β V |
24 | 12, 16, 17, 23 | ovmpo 7519 |
. . 3
β’ (([π΄] βΌ β (π / βΌ ) β§ [π΅] βΌ β (π / βΌ )) β ([π΄] βΌ (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)})[π΅] βΌ ) = βͺ {π§
β£ βπ β [
π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)}) |
25 | 7, 9, 24 | syl2anc 585 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ([π΄] βΌ (π₯ β (π / βΌ ), π¦ β (π / βΌ ) β¦ βͺ {π§
β£ βπ β
π₯ βπ β π¦ π§ = (ππ·π)})[π΅] βΌ ) = βͺ {π§
β£ βπ β [
π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)}) |
26 | | simpr3 1197 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π§ = (ππ·π)) |
27 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π· β (PsMetβπ)) |
28 | | simpr1 1195 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π β [π΄] βΌ ) |
29 | | metidss 32536 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π· β (PsMetβπ) β
(~Metβπ·)
β (π Γ π)) |
30 | 1, 29 | eqsstrid 3996 |
. . . . . . . . . . . . . . . . . . 19
β’ (π· β (PsMetβπ) β βΌ β (π Γ π)) |
31 | | xpss 5653 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Γ π) β (V Γ V) |
32 | 30, 31 | sstrdi 3960 |
. . . . . . . . . . . . . . . . . 18
β’ (π· β (PsMetβπ) β βΌ β (V Γ
V)) |
33 | | df-rel 5644 |
. . . . . . . . . . . . . . . . . 18
β’ (Rel
βΌ
β βΌ β (V Γ
V)) |
34 | 32, 33 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π· β (PsMetβπ) β Rel βΌ ) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β Rel βΌ ) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β Rel βΌ ) |
37 | | relelec 8699 |
. . . . . . . . . . . . . . 15
β’ (Rel
βΌ
β (π β [π΄] βΌ β π΄ βΌ π)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β (π β [π΄] βΌ β π΄ βΌ π)) |
39 | 28, 38 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π΄ βΌ π) |
40 | 1 | breqi 5115 |
. . . . . . . . . . . . 13
β’ (π΄ βΌ π β π΄(~Metβπ·)π) |
41 | 39, 40 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π΄(~Metβπ·)π) |
42 | | simpr2 1196 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π β [π΅] βΌ ) |
43 | | relelec 8699 |
. . . . . . . . . . . . . . 15
β’ (Rel
βΌ
β (π β [π΅] βΌ β π΅ βΌ π)) |
44 | 36, 43 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β (π β [π΅] βΌ β π΅ βΌ π)) |
45 | 42, 44 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π΅ βΌ π) |
46 | 1 | breqi 5115 |
. . . . . . . . . . . . 13
β’ (π΅ βΌ π β π΅(~Metβπ·)π) |
47 | 45, 46 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π΅(~Metβπ·)π) |
48 | | metideq 32538 |
. . . . . . . . . . . 12
β’ ((π· β (PsMetβπ) β§ (π΄(~Metβπ·)π β§ π΅(~Metβπ·)π)) β (π΄π·π΅) = (ππ·π)) |
49 | 27, 41, 47, 48 | syl12anc 836 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β (π΄π·π΅) = (ππ·π)) |
50 | 26, 49 | eqtr4d 2776 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π§ = (π΄π·π΅)) |
51 | 50 | adantlr 714 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) β§ (π β [π΄] βΌ β§ π β [π΅] βΌ β§ π§ = (ππ·π))) β π§ = (π΄π·π΅)) |
52 | 51 | 3anassrs 1361 |
. . . . . . . 8
β’
((((((π· β
(PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) β§ π β [π΄] βΌ ) β§ π β [π΅] βΌ ) β§ π§ = (ππ·π)) β π§ = (π΄π·π΅)) |
53 | | oveq1 7368 |
. . . . . . . . . . . 12
β’ (π = π β (ππ·π) = (ππ·π)) |
54 | 53 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = π β (π§ = (ππ·π) β π§ = (ππ·π))) |
55 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π = π β (ππ·π) = (ππ·π)) |
56 | 55 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = π β (π§ = (ππ·π) β π§ = (ππ·π))) |
57 | 54, 56 | cbvrex2vw 3227 |
. . . . . . . . . 10
β’
(βπ β [
π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) |
58 | 57 | biimpi 215 |
. . . . . . . . 9
β’
(βπ β [
π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) |
59 | 58 | adantl 483 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) |
60 | 52, 59 | r19.29vva 3204 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) β π§ = (π΄π·π΅)) |
61 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π· β (PsMetβπ)) |
62 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π΄ β π) |
63 | | psmet0 23684 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π΄ β π) β (π΄π·π΄) = 0) |
64 | 61, 62, 63 | syl2anc 585 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΄π·π΄) = 0) |
65 | | relelec 8699 |
. . . . . . . . . . 11
β’ (Rel
βΌ
β (π΄ β [π΄] βΌ β π΄ βΌ π΄)) |
66 | 61, 34, 65 | 3syl 18 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΄ β [π΄] βΌ β π΄ βΌ π΄)) |
67 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β βΌ =
(~Metβπ·)) |
68 | 67 | breqd 5120 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΄ βΌ π΄ β π΄(~Metβπ·)π΄)) |
69 | | metidv 32537 |
. . . . . . . . . . 11
β’ ((π· β (PsMetβπ) β§ (π΄ β π β§ π΄ β π)) β (π΄(~Metβπ·)π΄ β (π΄π·π΄) = 0)) |
70 | 61, 62, 62, 69 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΄(~Metβπ·)π΄ β (π΄π·π΄) = 0)) |
71 | 66, 68, 70 | 3bitrd 305 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΄ β [π΄] βΌ β (π΄π·π΄) = 0)) |
72 | 64, 71 | mpbird 257 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π΄ β [π΄] βΌ ) |
73 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π΅ β π) |
74 | | psmet0 23684 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π΅ β π) β (π΅π·π΅) = 0) |
75 | 61, 73, 74 | syl2anc 585 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΅π·π΅) = 0) |
76 | | relelec 8699 |
. . . . . . . . . . 11
β’ (Rel
βΌ
β (π΅ β [π΅] βΌ β π΅ βΌ π΅)) |
77 | 61, 34, 76 | 3syl 18 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΅ β [π΅] βΌ β π΅ βΌ π΅)) |
78 | 67 | breqd 5120 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΅ βΌ π΅ β π΅(~Metβπ·)π΅)) |
79 | | metidv 32537 |
. . . . . . . . . . 11
β’ ((π· β (PsMetβπ) β§ (π΅ β π β§ π΅ β π)) β (π΅(~Metβπ·)π΅ β (π΅π·π΅) = 0)) |
80 | 61, 73, 73, 79 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΅(~Metβπ·)π΅ β (π΅π·π΅) = 0)) |
81 | 77, 78, 80 | 3bitrd 305 |
. . . . . . . . 9
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β (π΅ β [π΅] βΌ β (π΅π·π΅) = 0)) |
82 | 75, 81 | mpbird 257 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π΅ β [π΅] βΌ ) |
83 | | simpr 486 |
. . . . . . . 8
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β π§ = (π΄π·π΅)) |
84 | | rspceov 7408 |
. . . . . . . 8
β’ ((π΄ β [π΄] βΌ β§ π΅ β [π΅] βΌ β§ π§ = (π΄π·π΅)) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) |
85 | 72, 82, 83, 84 | syl3anc 1372 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β§ π§ = (π΄π·π΅)) β βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)) |
86 | 60, 85 | impbida 800 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π) β π§ = (π΄π·π΅))) |
87 | 86 | abbidv 2802 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} = {π§ β£ π§ = (π΄π·π΅)}) |
88 | | df-sn 4591 |
. . . . 5
β’ {(π΄π·π΅)} = {π§ β£ π§ = (π΄π·π΅)} |
89 | 87, 88 | eqtr4di 2791 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} = {(π΄π·π΅)}) |
90 | 89 | unieqd 4883 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β βͺ {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} = βͺ {(π΄π·π΅)}) |
91 | | ovex 7394 |
. . . 4
β’ (π΄π·π΅) β V |
92 | 91 | unisn 4891 |
. . 3
β’ βͺ {(π΄π·π΅)} = (π΄π·π΅) |
93 | 90, 92 | eqtrdi 2789 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β βͺ {π§ β£ βπ β [ π΄] βΌ βπ β [ π΅] βΌ π§ = (ππ·π)} = (π΄π·π΅)) |
94 | 4, 25, 93 | 3eqtrd 2777 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ([π΄] βΌ
(pstoMetβπ·)[π΅] βΌ ) = (π΄π·π΅)) |