git @ Cat's Eye Technologies Eqthy / master eg / socks-and-shoes.eqthy.md
master

Tree @master (Download .tar.gz)

socks-and-shoes.eqthy.md @master — view rendered · raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Socks and Shoes
===============

<!--
SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->

See [Socks and shoes proof](https://en.wikiversity.org/wiki/Introduction_to_group_theory/Socks_and_shoes_proof)
on Wikiversity.

Also see [Inverse of Product](https://proofwiki.org/wiki/Inverse_of_Product) on ProofWiki.

Requires [Group theory](group-theory.eqthy.md).

    theorem (#socks-and-shoes)
        inv(mul(A, B)) = mul(inv(B), inv(A))
    proof
        e = e
        mul(A, inv(A)) = e

        mul(mul(A, B), inv(mul(A, B))) = e                 [by substitution of mul(A, B) into A]
        mul(mul(A, B), inv(mul(A, B))) = mul(A, inv(A))
        mul(mul(A, B), inv(mul(A, B))) = mul(mul(A, e), inv(A))
        mul(mul(A, B), inv(mul(A, B))) = mul(mul(A, mul(B, inv(B))), inv(A))  [by #inv-right with A=B]
        mul(mul(A, B), inv(mul(A, B))) = mul(mul(mul(A, B), inv(B)), inv(A))
        mul(mul(A, B), inv(mul(A, B))) = mul(mul(A, B), mul(inv(B), inv(A)))

        mul(inv(A), mul(mul(A, B), inv(mul(A, B)))) = mul(inv(A), mul(mul(A, B), mul(inv(B), inv(A))))  [by congruence of C and mul(inv(A), C)]
        mul(mul(inv(A), mul(A, B)), inv(mul(A, B))) = mul(inv(A), mul(mul(A, B), mul(inv(B), inv(A))))
        mul(mul(mul(inv(A), A), B), inv(mul(A, B))) = mul(inv(A), mul(mul(A, B), mul(inv(B), inv(A))))
        mul(mul(e, B), inv(mul(A, B))) = mul(inv(A), mul(mul(A, B), mul(inv(B), inv(A))))
        mul(B, inv(mul(A, B))) = mul(inv(A), mul(mul(A, B), mul(inv(B), inv(A))))

        mul(B, inv(mul(A, B))) = mul(mul(inv(A), mul(A, B)), mul(inv(B), inv(A)))
        mul(B, inv(mul(A, B))) = mul(mul(mul(inv(A), A), B), mul(inv(B), inv(A)))
        mul(B, inv(mul(A, B))) = mul(mul(e, B), mul(inv(B), inv(A)))
        mul(B, inv(mul(A, B))) = mul(B, mul(inv(B), inv(A)))

        mul(inv(B), mul(B, inv(mul(A, B)))) = mul(inv(B), mul(B, mul(inv(B), inv(A))))  [by congruence of C and mul(inv(B), C)]
        mul(mul(inv(B), B), inv(mul(A, B))) = mul(inv(B), mul(B, mul(inv(B), inv(A))))
        mul(mul(inv(B), B), inv(mul(A, B))) = mul(mul(inv(B), B), mul(inv(B), inv(A)))
        mul(e, inv(mul(A, B))) = mul(mul(inv(B), B), mul(inv(B), inv(A)))
        mul(e, inv(mul(A, B))) = mul(e, mul(inv(B), inv(A)))
        inv(mul(A, B)) = mul(e, mul(inv(B), inv(A)))
        inv(mul(A, B)) = mul(inv(B), inv(A))

    qed