Metamath Proof Explorer


Theorem grprinvlem

Description: Lemma for grprinvd . (Contributed by NM, 9-Aug-2013)

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

Proof

Step Hyp Ref Expression
1 grprinvlem.c ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
2 grprinvlem.o ( 𝜑𝑂𝐵 )
3 grprinvlem.i ( ( 𝜑𝑥𝐵 ) → ( 𝑂 + 𝑥 ) = 𝑥 )
4 grprinvlem.a ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5 grprinvlem.n ( ( 𝜑𝑥𝐵 ) → ∃ 𝑦𝐵 ( 𝑦 + 𝑥 ) = 𝑂 )
6 grprinvlem.x ( ( 𝜑𝜓 ) → 𝑋𝐵 )
7 grprinvlem.e ( ( 𝜑𝜓 ) → ( 𝑋 + 𝑋 ) = 𝑋 )
8 5 ralrimiva ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 ( 𝑦 + 𝑥 ) = 𝑂 )
9 oveq2 ( 𝑥 = 𝑧 → ( 𝑦 + 𝑥 ) = ( 𝑦 + 𝑧 ) )
10 9 eqeq1d ( 𝑥 = 𝑧 → ( ( 𝑦 + 𝑥 ) = 𝑂 ↔ ( 𝑦 + 𝑧 ) = 𝑂 ) )
11 10 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑦𝐵 ( 𝑦 + 𝑥 ) = 𝑂 ↔ ∃ 𝑦𝐵 ( 𝑦 + 𝑧 ) = 𝑂 ) )
12 11 cbvralvw ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑦 + 𝑥 ) = 𝑂 ↔ ∀ 𝑧𝐵𝑦𝐵 ( 𝑦 + 𝑧 ) = 𝑂 )
13 8 12 sylib ( 𝜑 → ∀ 𝑧𝐵𝑦𝐵 ( 𝑦 + 𝑧 ) = 𝑂 )
14 oveq2 ( 𝑧 = 𝑋 → ( 𝑦 + 𝑧 ) = ( 𝑦 + 𝑋 ) )
15 14 eqeq1d ( 𝑧 = 𝑋 → ( ( 𝑦 + 𝑧 ) = 𝑂 ↔ ( 𝑦 + 𝑋 ) = 𝑂 ) )
16 15 rexbidv ( 𝑧 = 𝑋 → ( ∃ 𝑦𝐵 ( 𝑦 + 𝑧 ) = 𝑂 ↔ ∃ 𝑦𝐵 ( 𝑦 + 𝑋 ) = 𝑂 ) )
17 16 rspccva ( ( ∀ 𝑧𝐵𝑦𝐵 ( 𝑦 + 𝑧 ) = 𝑂𝑋𝐵 ) → ∃ 𝑦𝐵 ( 𝑦 + 𝑋 ) = 𝑂 )
18 13 6 17 syl2an2r ( ( 𝜑𝜓 ) → ∃ 𝑦𝐵 ( 𝑦 + 𝑋 ) = 𝑂 )
19 7 oveq2d ( ( 𝜑𝜓 ) → ( 𝑦 + ( 𝑋 + 𝑋 ) ) = ( 𝑦 + 𝑋 ) )
20 19 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( 𝑦 + ( 𝑋 + 𝑋 ) ) = ( 𝑦 + 𝑋 ) )
21 simprr ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( 𝑦 + 𝑋 ) = 𝑂 )
22 21 oveq1d ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( ( 𝑦 + 𝑋 ) + 𝑋 ) = ( 𝑂 + 𝑋 ) )
23 4 caovassg ( ( 𝜑 ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
24 23 ad4ant14 ( ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
25 simprl ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → 𝑦𝐵 )
26 6 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → 𝑋𝐵 )
27 24 25 26 26 caovassd ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( ( 𝑦 + 𝑋 ) + 𝑋 ) = ( 𝑦 + ( 𝑋 + 𝑋 ) ) )
28 oveq2 ( 𝑦 = 𝑋 → ( 𝑂 + 𝑦 ) = ( 𝑂 + 𝑋 ) )
29 id ( 𝑦 = 𝑋𝑦 = 𝑋 )
30 28 29 eqeq12d ( 𝑦 = 𝑋 → ( ( 𝑂 + 𝑦 ) = 𝑦 ↔ ( 𝑂 + 𝑋 ) = 𝑋 ) )
31 3 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( 𝑂 + 𝑥 ) = 𝑥 )
32 oveq2 ( 𝑥 = 𝑦 → ( 𝑂 + 𝑥 ) = ( 𝑂 + 𝑦 ) )
33 id ( 𝑥 = 𝑦𝑥 = 𝑦 )
34 32 33 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝑂 + 𝑥 ) = 𝑥 ↔ ( 𝑂 + 𝑦 ) = 𝑦 ) )
35 34 cbvralvw ( ∀ 𝑥𝐵 ( 𝑂 + 𝑥 ) = 𝑥 ↔ ∀ 𝑦𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
36 31 35 sylib ( 𝜑 → ∀ 𝑦𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
37 36 adantr ( ( 𝜑𝜓 ) → ∀ 𝑦𝐵 ( 𝑂 + 𝑦 ) = 𝑦 )
38 30 37 6 rspcdva ( ( 𝜑𝜓 ) → ( 𝑂 + 𝑋 ) = 𝑋 )
39 38 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( 𝑂 + 𝑋 ) = 𝑋 )
40 22 27 39 3eqtr3d ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → ( 𝑦 + ( 𝑋 + 𝑋 ) ) = 𝑋 )
41 20 40 21 3eqtr3d ( ( ( 𝜑𝜓 ) ∧ ( 𝑦𝐵 ∧ ( 𝑦 + 𝑋 ) = 𝑂 ) ) → 𝑋 = 𝑂 )
42 18 41 rexlimddv ( ( 𝜑𝜓 ) → 𝑋 = 𝑂 )