Metamath Proof Explorer

Theorem caovmo

Description: Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of Gleason p. 119. (Contributed by NM, 4-Mar-1996)

Ref Expression
Hypotheses caovmo.2 
|- B e. S
caovmo.dom 
|- dom F = ( S X. S )
caovmo.3 
|- -. (/) e. S
caovmo.com 
|- ( x F y ) = ( y F x )
caovmo.ass 
|- ( ( x F y ) F z ) = ( x F ( y F z ) )
caovmo.id 
|- ( x e. S -> ( x F B ) = x )
Assertion caovmo 
|- E* w ( A F w ) = B

Proof

Step Hyp Ref Expression
1 caovmo.2 
 |-  B e. S
2 caovmo.dom 
 |-  dom F = ( S X. S )
3 caovmo.3 
 |-  -. (/) e. S
4 caovmo.com 
 |-  ( x F y ) = ( y F x )
5 caovmo.ass 
 |-  ( ( x F y ) F z ) = ( x F ( y F z ) )
6 caovmo.id 
 |-  ( x e. S -> ( x F B ) = x )
7 oveq1 
 |-  ( u = A -> ( u F w ) = ( A F w ) )
8 7 eqeq1d 
 |-  ( u = A -> ( ( u F w ) = B <-> ( A F w ) = B ) )
9 8 mobidv 
 |-  ( u = A -> ( E* w ( u F w ) = B <-> E* w ( A F w ) = B ) )
10 oveq2 
 |-  ( w = v -> ( u F w ) = ( u F v ) )
11 10 eqeq1d 
 |-  ( w = v -> ( ( u F w ) = B <-> ( u F v ) = B ) )
12 11 mo4 
 |-  ( E* w ( u F w ) = B <-> A. w A. v ( ( ( u F w ) = B /\ ( u F v ) = B ) -> w = v ) )
13 simpr 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u F v ) = B )
14 13 oveq2d 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( w F ( u F v ) ) = ( w F B ) )
15 simpl 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u F w ) = B )
16 15 oveq1d 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( ( u F w ) F v ) = ( B F v ) )
17 vex 
 |-  u e. _V
18 vex 
 |-  w e. _V
19 vex 
 |-  v e. _V
20 17 18 19 5 caovass 
 |-  ( ( u F w ) F v ) = ( u F ( w F v ) )
21 17 18 19 4 5 caov12 
 |-  ( u F ( w F v ) ) = ( w F ( u F v ) )
22 20 21 eqtri 
 |-  ( ( u F w ) F v ) = ( w F ( u F v ) )
23 1 elexi 
 |-  B e. _V
24 23 19 4 caovcom 
 |-  ( B F v ) = ( v F B )
25 16 22 24 3eqtr3g 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( w F ( u F v ) ) = ( v F B ) )
26 14 25 eqtr3d 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( w F B ) = ( v F B ) )
27 15 1 eqeltrdi 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u F w ) e. S )
28 2 3 ndmovrcl 
 |-  ( ( u F w ) e. S -> ( u e. S /\ w e. S ) )
29 27 28 syl 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u e. S /\ w e. S ) )
30 oveq1 
 |-  ( x = w -> ( x F B ) = ( w F B ) )
31 id 
 |-  ( x = w -> x = w )
32 30 31 eqeq12d 
 |-  ( x = w -> ( ( x F B ) = x <-> ( w F B ) = w ) )
33 32 6 vtoclga 
 |-  ( w e. S -> ( w F B ) = w )
34 29 33 simpl2im 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( w F B ) = w )
35 13 1 eqeltrdi 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u F v ) e. S )
36 2 3 ndmovrcl 
 |-  ( ( u F v ) e. S -> ( u e. S /\ v e. S ) )
37 35 36 syl 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( u e. S /\ v e. S ) )
38 oveq1 
 |-  ( x = v -> ( x F B ) = ( v F B ) )
39 id 
 |-  ( x = v -> x = v )
40 38 39 eqeq12d 
 |-  ( x = v -> ( ( x F B ) = x <-> ( v F B ) = v ) )
41 40 6 vtoclga 
 |-  ( v e. S -> ( v F B ) = v )
42 37 41 simpl2im 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> ( v F B ) = v )
43 26 34 42 3eqtr3d 
 |-  ( ( ( u F w ) = B /\ ( u F v ) = B ) -> w = v )
44 43 ax-gen 
 |-  A. v ( ( ( u F w ) = B /\ ( u F v ) = B ) -> w = v )
45 12 44 mpgbir 
 |-  E* w ( u F w ) = B
46 9 45 vtoclg 
 |-  ( A e. S -> E* w ( A F w ) = B )
47 moanimv 
 |-  ( E* w ( A e. S /\ ( A F w ) = B ) <-> ( A e. S -> E* w ( A F w ) = B ) )
48 46 47 mpbir 
 |-  E* w ( A e. S /\ ( A F w ) = B )
49 eleq1 
 |-  ( ( A F w ) = B -> ( ( A F w ) e. S <-> B e. S ) )
50 1 49 mpbiri 
 |-  ( ( A F w ) = B -> ( A F w ) e. S )
51 2 3 ndmovrcl 
 |-  ( ( A F w ) e. S -> ( A e. S /\ w e. S ) )
52 50 51 syl 
 |-  ( ( A F w ) = B -> ( A e. S /\ w e. S ) )
53 52 simpld 
 |-  ( ( A F w ) = B -> A e. S )
54 53 ancri 
 |-  ( ( A F w ) = B -> ( A e. S /\ ( A F w ) = B ) )
55 54 moimi 
 |-  ( E* w ( A e. S /\ ( A F w ) = B ) -> E* w ( A F w ) = B )
56 48 55 ax-mp 
 |-  E* w ( A F w ) = B