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 ⊢ ∃* 𝑤 ( 𝐴 𝐹 𝑤 ) = 𝐵