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

Metamath Proof Explorer

Theorem symggrplem

Description: Lemma for symggrp and efmndsgrp . Conditions for an operation to be associative. Formerly part of proof for symggrp . (Contributed by AV, 28-Jan-2024)

Ref Expression
Hypotheses symggrplem.c ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
symggrplem.p ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
Assertion symggrplem ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 symggrplem.c ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
2 symggrplem.p ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
3 coass ⊢ ( ( 𝑋 ∘ 𝑌 ) ∘ 𝑍 ) = ( 𝑋 ∘ ( 𝑌 ∘ 𝑍 ) )
4 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + 𝑦 ) = ( 𝑋 + 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑋 + 𝑦 ) ∈ 𝐵 ) )
6 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
7 6 eleq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) )
8 5 7 1 vtocl2ga ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
9 oveq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → ( 𝑥 + 𝑦 ) = ( ( 𝑋 + 𝑌 ) + 𝑦 ) )
10 coeq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → ( 𝑥 ∘ 𝑦 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑦 ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → ( ( 𝑥 + 𝑦 ) = ( 𝑥 ∘ 𝑦 ) ↔ ( ( 𝑋 + 𝑌 ) + 𝑦 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑦 ) ) )
12 oveq2 ⊢ ( 𝑦 = 𝑍 → ( ( 𝑋 + 𝑌 ) + 𝑦 ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
13 coeq2 ⊢ ( 𝑦 = 𝑍 → ( ( 𝑋 + 𝑌 ) ∘ 𝑦 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑍 ) )
14 12 13 eqeq12d ⊢ ( 𝑦 = 𝑍 → ( ( ( 𝑋 + 𝑌 ) + 𝑦 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑦 ) ↔ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑍 ) ) )
15 11 14 2 vtocl2ga ⊢ ( ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑍 ) )
16 8 15 stoic3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑌 ) ∘ 𝑍 ) )
17 coeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘ 𝑦 ) = ( 𝑋 ∘ 𝑦 ) )
18 4 17 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 𝑦 ) = ( 𝑥 ∘ 𝑦 ) ↔ ( 𝑋 + 𝑦 ) = ( 𝑋 ∘ 𝑦 ) ) )
19 coeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∘ 𝑦 ) = ( 𝑋 ∘ 𝑌 ) )
20 6 19 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 + 𝑦 ) = ( 𝑋 ∘ 𝑦 ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) ) )
21 18 20 2 vtocl2ga ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
22 21 3adant3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
23 22 coeq1d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) ∘ 𝑍 ) = ( ( 𝑋 ∘ 𝑌 ) ∘ 𝑍 ) )
24 16 23 eqtrd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 ∘ 𝑌 ) ∘ 𝑍 ) )
25 simp1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
26 oveq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 + 𝑦 ) = ( 𝑌 + 𝑦 ) )
27 26 eleq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑌 + 𝑦 ) ∈ 𝐵 ) )
28 oveq2 ⊢ ( 𝑦 = 𝑍 → ( 𝑌 + 𝑦 ) = ( 𝑌 + 𝑍 ) )
29 28 eleq1d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑌 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑌 + 𝑍 ) ∈ 𝐵 ) )
30 27 29 1 vtocl2ga ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) ∈ 𝐵 )
31 30 3adant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) ∈ 𝐵 )
32 oveq2 ⊢ ( 𝑦 = ( 𝑌 + 𝑍 ) → ( 𝑋 + 𝑦 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
33 coeq2 ⊢ ( 𝑦 = ( 𝑌 + 𝑍 ) → ( 𝑋 ∘ 𝑦 ) = ( 𝑋 ∘ ( 𝑌 + 𝑍 ) ) )
34 32 33 eqeq12d ⊢ ( 𝑦 = ( 𝑌 + 𝑍 ) → ( ( 𝑋 + 𝑦 ) = ( 𝑋 ∘ 𝑦 ) ↔ ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 ∘ ( 𝑌 + 𝑍 ) ) ) )
35 18 34 2 vtocl2ga ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 + 𝑍 ) ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 ∘ ( 𝑌 + 𝑍 ) ) )
36 25 31 35 syl2anc ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 ∘ ( 𝑌 + 𝑍 ) ) )
37 coeq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∘ 𝑦 ) = ( 𝑌 ∘ 𝑦 ) )
38 26 37 eqeq12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 + 𝑦 ) = ( 𝑥 ∘ 𝑦 ) ↔ ( 𝑌 + 𝑦 ) = ( 𝑌 ∘ 𝑦 ) ) )
39 coeq2 ⊢ ( 𝑦 = 𝑍 → ( 𝑌 ∘ 𝑦 ) = ( 𝑌 ∘ 𝑍 ) )
40 28 39 eqeq12d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑌 + 𝑦 ) = ( 𝑌 ∘ 𝑦 ) ↔ ( 𝑌 + 𝑍 ) = ( 𝑌 ∘ 𝑍 ) ) )
41 38 40 2 vtocl2ga ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) = ( 𝑌 ∘ 𝑍 ) )
42 41 3adant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 + 𝑍 ) = ( 𝑌 ∘ 𝑍 ) )
43 42 coeq2d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∘ ( 𝑌 + 𝑍 ) ) = ( 𝑋 ∘ ( 𝑌 ∘ 𝑍 ) ) )
44 36 43 eqtrd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 ∘ ( 𝑌 ∘ 𝑍 ) ) )
45 3 24 44 3eqtr4a ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )