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

Metamath Proof Explorer

Theorem caovmo

Proof