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 𝐵𝑆
caovmo.dom dom 𝐹 = ( 𝑆 × 𝑆 )
caovmo.3 ¬ ∅ ∈ 𝑆
caovmo.com ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
caovmo.ass ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
caovmo.id ( 𝑥𝑆 → ( 𝑥 𝐹 𝐵 ) = 𝑥 )
Assertion caovmo ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵

Proof

Step Hyp Ref Expression
1 caovmo.2 𝐵𝑆
2 caovmo.dom dom 𝐹 = ( 𝑆 × 𝑆 )
3 caovmo.3 ¬ ∅ ∈ 𝑆
4 caovmo.com ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
5 caovmo.ass ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
6 caovmo.id ( 𝑥𝑆 → ( 𝑥 𝐹 𝐵 ) = 𝑥 )
7 oveq1 ( 𝑢 = 𝐴 → ( 𝑢 𝐹 𝑤 ) = ( 𝐴 𝐹 𝑤 ) )
8 7 eqeq1d ( 𝑢 = 𝐴 → ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ↔ ( 𝐴 𝐹 𝑤 ) = 𝐵 ) )
9 8 mobidv ( 𝑢 = 𝐴 → ( ∃* 𝑤 ( 𝑢 𝐹 𝑤 ) = 𝐵 ↔ ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵 ) )
10 oveq2 ( 𝑤 = 𝑣 → ( 𝑢 𝐹 𝑤 ) = ( 𝑢 𝐹 𝑣 ) )
11 10 eqeq1d ( 𝑤 = 𝑣 → ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ↔ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) )
12 11 mo4 ( ∃* 𝑤 ( 𝑢 𝐹 𝑤 ) = 𝐵 ↔ ∀ 𝑤𝑣 ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → 𝑤 = 𝑣 ) )
13 simpr ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢 𝐹 𝑣 ) = 𝐵 )
14 13 oveq2d ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑤 𝐹 ( 𝑢 𝐹 𝑣 ) ) = ( 𝑤 𝐹 𝐵 ) )
15 simpl ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢 𝐹 𝑤 ) = 𝐵 )
16 15 oveq1d ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( ( 𝑢 𝐹 𝑤 ) 𝐹 𝑣 ) = ( 𝐵 𝐹 𝑣 ) )
17 vex 𝑢 ∈ V
18 vex 𝑤 ∈ V
19 vex 𝑣 ∈ V
20 17 18 19 5 caovass ( ( 𝑢 𝐹 𝑤 ) 𝐹 𝑣 ) = ( 𝑢 𝐹 ( 𝑤 𝐹 𝑣 ) )
21 17 18 19 4 5 caov12 ( 𝑢 𝐹 ( 𝑤 𝐹 𝑣 ) ) = ( 𝑤 𝐹 ( 𝑢 𝐹 𝑣 ) )
22 20 21 eqtri ( ( 𝑢 𝐹 𝑤 ) 𝐹 𝑣 ) = ( 𝑤 𝐹 ( 𝑢 𝐹 𝑣 ) )
23 1 elexi 𝐵 ∈ V
24 23 19 4 caovcom ( 𝐵 𝐹 𝑣 ) = ( 𝑣 𝐹 𝐵 )
25 16 22 24 3eqtr3g ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑤 𝐹 ( 𝑢 𝐹 𝑣 ) ) = ( 𝑣 𝐹 𝐵 ) )
26 14 25 eqtr3d ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑤 𝐹 𝐵 ) = ( 𝑣 𝐹 𝐵 ) )
27 15 1 eqeltrdi ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢 𝐹 𝑤 ) ∈ 𝑆 )
28 2 3 ndmovrcl ( ( 𝑢 𝐹 𝑤 ) ∈ 𝑆 → ( 𝑢𝑆𝑤𝑆 ) )
29 27 28 syl ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢𝑆𝑤𝑆 ) )
30 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 𝐹 𝐵 ) = ( 𝑤 𝐹 𝐵 ) )
31 id ( 𝑥 = 𝑤𝑥 = 𝑤 )
32 30 31 eqeq12d ( 𝑥 = 𝑤 → ( ( 𝑥 𝐹 𝐵 ) = 𝑥 ↔ ( 𝑤 𝐹 𝐵 ) = 𝑤 ) )
33 32 6 vtoclga ( 𝑤𝑆 → ( 𝑤 𝐹 𝐵 ) = 𝑤 )
34 29 33 simpl2im ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑤 𝐹 𝐵 ) = 𝑤 )
35 13 1 eqeltrdi ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢 𝐹 𝑣 ) ∈ 𝑆 )
36 2 3 ndmovrcl ( ( 𝑢 𝐹 𝑣 ) ∈ 𝑆 → ( 𝑢𝑆𝑣𝑆 ) )
37 35 36 syl ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑢𝑆𝑣𝑆 ) )
38 oveq1 ( 𝑥 = 𝑣 → ( 𝑥 𝐹 𝐵 ) = ( 𝑣 𝐹 𝐵 ) )
39 id ( 𝑥 = 𝑣𝑥 = 𝑣 )
40 38 39 eqeq12d ( 𝑥 = 𝑣 → ( ( 𝑥 𝐹 𝐵 ) = 𝑥 ↔ ( 𝑣 𝐹 𝐵 ) = 𝑣 ) )
41 40 6 vtoclga ( 𝑣𝑆 → ( 𝑣 𝐹 𝐵 ) = 𝑣 )
42 37 41 simpl2im ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → ( 𝑣 𝐹 𝐵 ) = 𝑣 )
43 26 34 42 3eqtr3d ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → 𝑤 = 𝑣 )
44 43 ax-gen 𝑣 ( ( ( 𝑢 𝐹 𝑤 ) = 𝐵 ∧ ( 𝑢 𝐹 𝑣 ) = 𝐵 ) → 𝑤 = 𝑣 )
45 12 44 mpgbir ∃* 𝑤 ( 𝑢 𝐹 𝑤 ) = 𝐵
46 9 45 vtoclg ( 𝐴𝑆 → ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵 )
47 moanimv ( ∃* 𝑤 ( 𝐴𝑆 ∧ ( 𝐴 𝐹 𝑤 ) = 𝐵 ) ↔ ( 𝐴𝑆 → ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵 ) )
48 46 47 mpbir ∃* 𝑤 ( 𝐴𝑆 ∧ ( 𝐴 𝐹 𝑤 ) = 𝐵 )
49 eleq1 ( ( 𝐴 𝐹 𝑤 ) = 𝐵 → ( ( 𝐴 𝐹 𝑤 ) ∈ 𝑆𝐵𝑆 ) )
50 1 49 mpbiri ( ( 𝐴 𝐹 𝑤 ) = 𝐵 → ( 𝐴 𝐹 𝑤 ) ∈ 𝑆 )
51 2 3 ndmovrcl ( ( 𝐴 𝐹 𝑤 ) ∈ 𝑆 → ( 𝐴𝑆𝑤𝑆 ) )
52 50 51 syl ( ( 𝐴 𝐹 𝑤 ) = 𝐵 → ( 𝐴𝑆𝑤𝑆 ) )
53 52 simpld ( ( 𝐴 𝐹 𝑤 ) = 𝐵𝐴𝑆 )
54 53 ancri ( ( 𝐴 𝐹 𝑤 ) = 𝐵 → ( 𝐴𝑆 ∧ ( 𝐴 𝐹 𝑤 ) = 𝐵 ) )
55 54 moimi ( ∃* 𝑤 ( 𝐴𝑆 ∧ ( 𝐴 𝐹 𝑤 ) = 𝐵 ) → ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵 )
56 48 55 ax-mp ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵