Metamath Proof Explorer

Theorem grprinvd

Description: Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013) (Proof shortened by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grprinvlem.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
grprinvlem.o ⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )
grprinvlem.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 + 𝑥 ) = 𝑥 )
grprinvlem.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
grprinvlem.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 𝑂 )
grprinvd.x ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐵 )
grprinvd.n ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ 𝐵 )
grprinvd.e ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 + 𝑋 ) = 𝑂 )
Assertion grprinvd ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 + 𝑁 ) = 𝑂 )

Proof

Step Hyp Ref Expression
1 grprinvlem.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
2 grprinvlem.o ⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )
3 grprinvlem.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 + 𝑥 ) = 𝑥 )
4 grprinvlem.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5 grprinvlem.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 𝑂 )
6 grprinvd.x ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐵 )
7 grprinvd.n ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ 𝐵 )
8 grprinvd.e ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 + 𝑋 ) = 𝑂 )
9 1 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
10 9 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
12 11 6 7 caovcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 + 𝑁 ) ∈ 𝐵 )
13 4 caovassg ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
14 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
15 14 6 7 12 caovassd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 + 𝑁 ) + ( 𝑋 + 𝑁 ) ) = ( 𝑋 + ( 𝑁 + ( 𝑋 + 𝑁 ) ) ) )
16 8 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 𝑋 ) + 𝑁 ) = ( 𝑂 + 𝑁 ) )
17 14 7 6 7 caovassd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 𝑋 ) + 𝑁 ) = ( 𝑁 + ( 𝑋 + 𝑁 ) ) )
18 oveq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑂 + 𝑦 ) = ( 𝑂 + 𝑁 ) )
19 id ⊢ ( 𝑦 = 𝑁 → 𝑦 = 𝑁 )
20 18 19 eqeq12d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑂 + 𝑦 ) = 𝑦 ↔ ( 𝑂 + 𝑁 ) = 𝑁 ) )
21 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑂 + 𝑥 ) = 𝑥 )
22 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑂 + 𝑥 ) = ( 𝑂 + 𝑦 ) )
23 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
24 22 23 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑂 + 𝑥 ) = 𝑥 ↔ ( 𝑂 + 𝑦 ) = 𝑦 ) )
25 24 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑂 + 𝑥 ) = 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
26 21 25 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
28 20 27 7 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 + 𝑁 ) = 𝑁 )
29 16 17 28 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 + ( 𝑋 + 𝑁 ) ) = 𝑁 )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 + ( 𝑁 + ( 𝑋 + 𝑁 ) ) ) = ( 𝑋 + 𝑁 ) )
31 15 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 + 𝑁 ) + ( 𝑋 + 𝑁 ) ) = ( 𝑋 + 𝑁 ) )
32 1 2 3 4 5 12 31 grprinvlem ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 + 𝑁 ) = 𝑂 )