Step | Hyp | Ref
| Expression |
1 | | oppglsm.o |
. . . . . . 7
β’ π =
(oppgβπΊ) |
2 | 1 | fvexi 6860 |
. . . . . 6
β’ π β V |
3 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
4 | 1, 3 | oppgbas 19138 |
. . . . . . 7
β’
(BaseβπΊ) =
(Baseβπ) |
5 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
6 | | eqid 2733 |
. . . . . . 7
β’
(LSSumβπ) =
(LSSumβπ) |
7 | 4, 5, 6 | lsmfval 19428 |
. . . . . 6
β’ (π β V β
(LSSumβπ) = (π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦ ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)))) |
8 | 2, 7 | ax-mp 5 |
. . . . 5
β’
(LSSumβπ) =
(π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦ ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦))) |
9 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
10 | | oppglsm.p |
. . . . . . . 8
β’ β =
(LSSumβπΊ) |
11 | 3, 9, 10 | lsmfval 19428 |
. . . . . . 7
β’ (πΊ β V β β =
(π’ β π«
(BaseβπΊ), π‘ β π«
(BaseβπΊ) β¦ ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)))) |
12 | 11 | tposeqd 8164 |
. . . . . 6
β’ (πΊ β V β tpos β = tpos
(π’ β π«
(BaseβπΊ), π‘ β π«
(BaseβπΊ) β¦ ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)))) |
13 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
14 | 13 | reldmmpo 7494 |
. . . . . . . . . . . 12
β’ Rel dom
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
15 | 13 | mpofun 7484 |
. . . . . . . . . . . . 13
β’ Fun
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
16 | | funforn 6767 |
. . . . . . . . . . . . 13
β’ (Fun
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) β (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))) |
17 | 15, 16 | mpbi 229 |
. . . . . . . . . . . 12
β’ (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
18 | | tposfo2 8184 |
. . . . . . . . . . . 12
β’ (Rel dom
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) β ((π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) β tpos (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):β‘dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)))) |
19 | 14, 17, 18 | mp2 9 |
. . . . . . . . . . 11
β’ tpos
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):β‘dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
20 | | forn 6763 |
. . . . . . . . . . 11
β’ (tpos
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)):β‘dom (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))βontoβran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) β ran tpos (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = ran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . 10
β’ ran tpos
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = ran (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) |
22 | 9, 1, 5 | oppgplus 19135 |
. . . . . . . . . . . . . . 15
β’ (π₯(+gβπ)π¦) = (π¦(+gβπΊ)π₯) |
23 | 22 | eqcomi 2742 |
. . . . . . . . . . . . . 14
β’ (π¦(+gβπΊ)π₯) = (π₯(+gβπ)π¦) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π¦ β π’ β§ π₯ β π‘) β (π¦(+gβπΊ)π₯) = (π₯(+gβπ)π¦)) |
25 | 24 | mpoeq3ia 7439 |
. . . . . . . . . . . 12
β’ (π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = (π¦ β π’, π₯ β π‘ β¦ (π₯(+gβπ)π¦)) |
26 | 25 | tposmpo 8198 |
. . . . . . . . . . 11
β’ tpos
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) |
27 | 26 | rneqi 5896 |
. . . . . . . . . 10
β’ ran tpos
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) |
28 | 21, 27 | eqtr3i 2763 |
. . . . . . . . 9
β’ ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) |
29 | 28 | a1i 11 |
. . . . . . . 8
β’ ((π’ β π«
(BaseβπΊ) β§ π‘ β π«
(BaseβπΊ)) β ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯)) = ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦))) |
30 | 29 | mpoeq3ia 7439 |
. . . . . . 7
β’ (π’ β π«
(BaseβπΊ), π‘ β π«
(BaseβπΊ) β¦ ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))) = (π’ β π« (BaseβπΊ), π‘ β π« (BaseβπΊ) β¦ ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦))) |
31 | 30 | tposmpo 8198 |
. . . . . 6
β’ tpos
(π’ β π«
(BaseβπΊ), π‘ β π«
(BaseβπΊ) β¦ ran
(π¦ β π’, π₯ β π‘ β¦ (π¦(+gβπΊ)π₯))) = (π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦))) |
32 | 12, 31 | eqtrdi 2789 |
. . . . 5
β’ (πΊ β V β tpos β =
(π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦ ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)))) |
33 | 8, 32 | eqtr4id 2792 |
. . . 4
β’ (πΊ β V β
(LSSumβπ) = tpos
β
) |
34 | 33 | oveqd 7378 |
. . 3
β’ (πΊ β V β (π(LSSumβπ)π) = (πtpos β π)) |
35 | | ovtpos 8176 |
. . 3
β’ (πtpos β π) = (π β π) |
36 | 34, 35 | eqtrdi 2789 |
. 2
β’ (πΊ β V β (π(LSSumβπ)π) = (π β π)) |
37 | | eqid 2733 |
. . . . . . 7
β’ (π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦
β
) = (π‘ β
π« (BaseβπΊ),
π’ β π«
(BaseβπΊ) β¦
β
) |
38 | | 0ex 5268 |
. . . . . . 7
β’ β
β V |
39 | | eqidd 2734 |
. . . . . . 7
β’ ((π‘ = π β§ π’ = π) β β
= β
) |
40 | 37, 38, 39 | elovmpo 7602 |
. . . . . 6
β’ (π₯ β (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) β (π β π« (BaseβπΊ) β§ π β π« (BaseβπΊ) β§ π₯ β β
)) |
41 | 40 | simp3bi 1148 |
. . . . 5
β’ (π₯ β (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) β π₯ β β
) |
42 | 41 | ssriv 3952 |
. . . 4
β’ (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) β
β
|
43 | | ss0 4362 |
. . . 4
β’ ((π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) β β
β (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) = β
) |
44 | 42, 43 | ax-mp 5 |
. . 3
β’ (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π) = β
|
45 | | elpwi 4571 |
. . . . . . . . . . . . 13
β’ (π‘ β π«
(BaseβπΊ) β π‘ β (BaseβπΊ)) |
46 | 45 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
π‘ β (BaseβπΊ)) |
47 | | fvprc 6838 |
. . . . . . . . . . . . 13
β’ (Β¬
πΊ β V β
(BaseβπΊ) =
β
) |
48 | 47 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
(BaseβπΊ) =
β
) |
49 | 46, 48 | sseqtrd 3988 |
. . . . . . . . . . 11
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
π‘ β
β
) |
50 | | ss0 4362 |
. . . . . . . . . . 11
β’ (π‘ β β
β π‘ = β
) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
π‘ =
β
) |
52 | 51 | orcd 872 |
. . . . . . . . 9
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
(π‘ = β
β¨ π’ = β
)) |
53 | | 0mpo0 7444 |
. . . . . . . . 9
β’ ((π‘ = β
β¨ π’ = β
) β (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) = β
) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) = β
) |
55 | 54 | rneqd 5897 |
. . . . . . 7
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) = ran β
) |
56 | | rn0 5885 |
. . . . . . 7
β’ ran
β
= β
|
57 | 55, 56 | eqtrdi 2789 |
. . . . . 6
β’ ((Β¬
πΊ β V β§ π‘ β π«
(BaseβπΊ) β§ π’ β π«
(BaseβπΊ)) β ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦)) = β
) |
58 | 57 | mpoeq3dva 7438 |
. . . . 5
β’ (Β¬
πΊ β V β (π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦ ran
(π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ)π¦))) = (π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦
β
)) |
59 | 8, 58 | eqtrid 2785 |
. . . 4
β’ (Β¬
πΊ β V β
(LSSumβπ) = (π‘ β π«
(BaseβπΊ), π’ β π«
(BaseβπΊ) β¦
β
)) |
60 | 59 | oveqd 7378 |
. . 3
β’ (Β¬
πΊ β V β (π(LSSumβπ)π) = (π(π‘ β π« (BaseβπΊ), π’ β π« (BaseβπΊ) β¦ β
)π)) |
61 | | fvprc 6838 |
. . . . . 6
β’ (Β¬
πΊ β V β
(LSSumβπΊ) =
β
) |
62 | 10, 61 | eqtrid 2785 |
. . . . 5
β’ (Β¬
πΊ β V β β =
β
) |
63 | 62 | oveqd 7378 |
. . . 4
β’ (Β¬
πΊ β V β (π β π) = (πβ
π)) |
64 | | 0ov 7398 |
. . . 4
β’ (πβ
π) = β
|
65 | 63, 64 | eqtrdi 2789 |
. . 3
β’ (Β¬
πΊ β V β (π β π) = β
) |
66 | 44, 60, 65 | 3eqtr4a 2799 |
. 2
β’ (Β¬
πΊ β V β (π(LSSumβπ)π) = (π β π)) |
67 | 36, 66 | pm2.61i 182 |
1
β’ (π(LSSumβπ)π) = (π β π) |