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 biimpi ⊢ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
25 24 adantr ⊢ ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑤 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑤 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
26 20 25 syl ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
27 26 ex ⊢ ( 𝑤 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
28 14 27 syldc ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( 𝑤 ∈ 𝐵 → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
29 28 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( 𝑤 ∈ 𝐵 → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 ) )
30 29 imp ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 )
31 eqeq2 ⊢ ( 𝑦 = 𝑎 → ( ( 𝑙 + 𝑤 ) = 𝑦 ↔ ( 𝑙 + 𝑤 ) = 𝑎 ) )
32 31 rexbidv ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ) )
33 eqeq2 ⊢ ( 𝑦 = 𝑎 → ( ( 𝑤 + 𝑟 ) = 𝑦 ↔ ( 𝑤 + 𝑟 ) = 𝑎 ) )
34 33 rexbidv ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
35 32 34 anbi12d ⊢ ( 𝑦 = 𝑎 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) ) )
36 12 35 rspc2va ⊢ ( ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑤 ) = 𝑎 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
37 36 simprd ⊢ ( ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
38 37 expcom ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
39 38 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑤 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ) )
40 39 impl ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
41 40 ad2ant2r ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 )
42 oveq2 ⊢ ( 𝑟 = 𝑧 → ( 𝑤 + 𝑟 ) = ( 𝑤 + 𝑧 ) )
43 42 eqeq1d ⊢ ( 𝑟 = 𝑧 → ( ( 𝑤 + 𝑟 ) = 𝑎 ↔ ( 𝑤 + 𝑧 ) = 𝑎 ) )
44 43 cbvrexvw ⊢ ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑤 + 𝑧 ) = 𝑎 )
45 simpll1 ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐺 ∈ Smgrp )
46 45 adantr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐺 ∈ Smgrp )
47 simplr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
48 simpllr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
49 simprr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
50 1 2 sgrpass ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑢 + ( 𝑤 + 𝑧 ) ) )
51 46 47 48 49 50 syl13anc ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑢 + ( 𝑤 + 𝑧 ) ) )
52 simprl ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑢 + 𝑤 ) = 𝑤 )
53 52 oveq1d ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑤 ) + 𝑧 ) = ( 𝑤 + 𝑧 ) )
54 51 53 eqtr3d ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑢 + 𝑤 ) = 𝑤 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
55 54 anassrs ⊢ ( ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
56 oveq2 ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑢 + 𝑎 ) )
57 id ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑤 + 𝑧 ) = 𝑎 )
58 56 57 eqeq12d ⊢ ( ( 𝑤 + 𝑧 ) = 𝑎 → ( ( 𝑢 + ( 𝑤 + 𝑧 ) ) = ( 𝑤 + 𝑧 ) ↔ ( 𝑢 + 𝑎 ) = 𝑎 ) )
59 55 58 syl5ibcom ⊢ ( ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
60 59 rexlimdva ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑤 + 𝑧 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
61 44 60 biimtrid ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
62 61 adantrl ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( ∃ 𝑟 ∈ 𝐵 ( 𝑤 + 𝑟 ) = 𝑎 → ( 𝑢 + 𝑎 ) = 𝑎 ) )
63 41 62 mpd ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( 𝑢 + 𝑎 ) = 𝑎 )
64 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑙 + 𝑥 ) = ( 𝑙 + 𝑎 ) )
65 64 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑙 + 𝑥 ) = 𝑦 ↔ ( 𝑙 + 𝑎 ) = 𝑦 ) )
66 65 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ) )
67 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 + 𝑟 ) = ( 𝑎 + 𝑟 ) )
68 67 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑎 + 𝑟 ) = 𝑦 ) )
69 68 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) )
70 66 69 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) ) )
71 eqeq2 ⊢ ( 𝑦 = 𝑢 → ( ( 𝑙 + 𝑎 ) = 𝑦 ↔ ( 𝑙 + 𝑎 ) = 𝑢 ) )
72 71 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ↔ ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
73 eqeq2 ⊢ ( 𝑦 = 𝑢 → ( ( 𝑎 + 𝑟 ) = 𝑦 ↔ ( 𝑎 + 𝑟 ) = 𝑢 ) )
74 73 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) )
75 72 74 anbi12d ⊢ ( 𝑦 = 𝑢 → ( ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑦 ) ↔ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) ) )
76 70 75 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑎 + 𝑟 ) = 𝑢 ) )
77 76 simpld ⊢ ( ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 )
78 77 ex ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
79 78 ancoms ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
80 79 com12 ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
81 80 3ad2ant3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ) )
82 81 impl ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 )
83 oveq1 ⊢ ( 𝑙 = 𝑖 → ( 𝑙 + 𝑎 ) = ( 𝑖 + 𝑎 ) )
84 83 eqeq1d ⊢ ( 𝑙 = 𝑖 → ( ( 𝑙 + 𝑎 ) = 𝑢 ↔ ( 𝑖 + 𝑎 ) = 𝑢 ) )
85 84 cbvrexvw ⊢ ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑎 ) = 𝑢 ↔ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
86 82 85 sylib ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
87 86 adantllr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
88 87 adantrr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 )
89 63 88 jca ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ ( 𝑢 + 𝑤 ) = 𝑤 ) ) → ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
90 89 expr ⊢ ( ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑢 + 𝑤 ) = 𝑤 → ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
91 90 ralrimdva ⊢ ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑢 + 𝑤 ) = 𝑤 → ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
92 91 reximdva ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝑢 + 𝑤 ) = 𝑤 → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
93 30 92 mpd ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
94 5 93 exlimddv ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )