This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinvalem

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

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

Proof

Step Hyp Ref Expression
1 grpinva.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
2 grpinva.o ⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )
3 grpinva.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 + 𝑥 ) = 𝑥 )
4 grpinva.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5 grpinva.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 𝑂 )
6 grpinvalem.x ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐵 )
7 grpinvalem.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 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 = 𝑂 )