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

Metamath Proof Explorer

Theorem dfgrp3lem

Description: Lemma for dfgrp3 . (Contributed by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
dfgrp3.p ⊢ + = ( +g ‘ 𝐺 )
Assertion dfgrp3lem ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )

Proof

Step Hyp Ref Expression
1 dfgrp3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 dfgrp3.p ⊢ + = ( +g ‘ 𝐺 )
3 simp2 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐵 ≠ ∅ )
4 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐵 )
5 3 4 sylib ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑤 𝑤 ∈ 𝐵 )
6 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑙 + 𝑥 ) = ( 𝑙 + 𝑤 ) )
7 6 eqeq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑙 + 𝑥 ) = 𝑦 ↔ ( 𝑙 + 𝑤 ) = 𝑦 ) )
8 7 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ) )
9 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 + 𝑟 ) = ( 𝑤 + 𝑟 ) )
10 9 eqeq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑤 + 𝑟 ) = 𝑦 ) )
11 10 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) )
12 8 11 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) )
13 12 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) )
14 13 rspcv ⊢ ( 𝑤 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) )
15 eqeq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝑙 + 𝑤 ) = 𝑦 ↔ ( 𝑙 + 𝑤 ) = 𝑤 ) )
16 15 rexbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ) )
17 eqeq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝑤 + 𝑟 ) = 𝑦 ↔ ( 𝑤 + 𝑟 ) = 𝑤 ) )
18 17 rexbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑤 ) )
19 16 18 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑤 ) ) )
20 19 rspcva ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑤 ) )
21 oveq1 ⊢ ( 𝑙 = 𝑢 → ( 𝑙 + 𝑤 ) = ( 𝑢 + 𝑤 ) )
22 21 eqeq1d ⊢ ( 𝑙 = 𝑢 → ( ( 𝑙 + 𝑤 ) = 𝑤 ↔ ( 𝑢 + 𝑤 ) = 𝑤 ) )
23 22 cbvrexvw ⊢ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
24 23 birani ⊢ ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑤 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
25 20 24 syl ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
26 25 ex ⊢ ( 𝑤 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
27 14 26 syldc ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( 𝑤 ∈ 𝐵 → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
28 27 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( 𝑤 ∈ 𝐵 → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
29 28 imp ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
30 eqeq2 ⊢ ( 𝑦 = 𝑎 → ( ( 𝑙 + 𝑤 ) = 𝑦 ↔ ( 𝑙 + 𝑤 ) = 𝑎 ) )
31 30 rexbidv ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ) )
32 eqeq2 ⊢ ( 𝑦 = 𝑎 → ( ( 𝑤 + 𝑟 ) = 𝑦 ↔ ( 𝑤 + 𝑟 ) = 𝑎 ) )
33 32 rexbidv ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
34 31 33 anbi12d ⊢ ( 𝑦 = 𝑎 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) ) )
35 12 34 rspc2va ⊢ ( ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
36 35 simprd ⊢ ( ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
37 36 expcom ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
38 37 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
39 38 impl ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
40 39 ad2ant2r ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
41 oveq2 ⊢ ( 𝑟 = 𝑧 → ( 𝑤 + 𝑟 ) = ( 𝑤 + 𝑧 ) )
42 41 eqeq1d ⊢ ( 𝑟 = 𝑧 → ( ( 𝑤 + 𝑟 ) = 𝑎 ↔ ( 𝑤 + 𝑧 ) = 𝑎 ) )
43 42 cbvrexvw ⊢ ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑤 + 𝑧 ) = 𝑎 )
44 simpll1 ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐺 ∈ Smgrp )
45 44 adantr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐺 ∈ Smgrp )
46 simplr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
47 simpllr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
48 simprr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
49 1 2 sgrpass ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑢 + ( 𝑤 + 𝑧 ) ) )
50 45 46 47 48 49 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑢 + ( 𝑤 + 𝑧 ) ) )
51 simprl ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑢 + 𝑤 ) = 𝑤 )
52 51 oveq1d ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑤 + 𝑧 ) )
53 50 52 eqtr3d ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
54 53 anassrs ⊢ ( ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
55 oveq2 ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑢 + 𝑎 ) )
56 id ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑤 + 𝑧 ) = 𝑎 )
57 55 56 eqeq12d ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) ↔ ( 𝑢 + 𝑎 ) = 𝑎 ) )
58 54 57 syl5ibcom ⊢ ( ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
59 58 rexlimdva ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
60 43 59 biimtrid ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
61 60 adantrl ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
62 40 61 mpd ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( 𝑢 + 𝑎 ) = 𝑎 )
63 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑙 + 𝑥 ) = ( 𝑙 + 𝑎 ) )
64 63 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑙 + 𝑥 ) = 𝑦 ↔ ( 𝑙 + 𝑎 ) = 𝑦 ) )
65 64 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ) )
66 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 + 𝑟 ) = ( 𝑎 + 𝑟 ) )
67 66 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑎 + 𝑟 ) = 𝑦 ) )
68 67 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) )
69 65 68 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) ) )
70 eqeq2 ⊢ ( 𝑦 = 𝑢 → ( ( 𝑙 + 𝑎 ) = 𝑦 ↔ ( 𝑙 + 𝑎 ) = 𝑢 ) )
71 70 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
72 eqeq2 ⊢ ( 𝑦 = 𝑢 → ( ( 𝑎 + 𝑟 ) = 𝑦 ↔ ( 𝑎 + 𝑟 ) = 𝑢 ) )
73 72 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) )
74 71 73 anbi12d ⊢ ( 𝑦 = 𝑢 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) ) )
75 69 74 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) )
76 75 simpld ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 )
77 76 ex ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
78 77 ancoms ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
79 78 com12 ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
80 79 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
81 80 impl ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 )
82 oveq1 ⊢ ( 𝑙 = 𝑖 → ( 𝑙 + 𝑎 ) = ( 𝑖 + 𝑎 ) )
83 82 eqeq1d ⊢ ( 𝑙 = 𝑖 → ( ( 𝑙 + 𝑎 ) = 𝑢 ↔ ( 𝑖 + 𝑎 ) = 𝑢 ) )
84 83 cbvrexvw ⊢ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ↔ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
85 81 84 sylib ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
86 85 adantllr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
87 86 adantrr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
88 62 87 jca ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
89 88 expr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑢 + 𝑤 ) = 𝑤 → ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
90 89 ralrimdva ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑢 + 𝑤 ) = 𝑤 → ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
91 90 reximdva ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
92 29 91 mpd ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
93 5 92 exlimddv ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )