Metamath Proof Explorer

Theorem cyccom

Description: Condition for an operation to be commutative. Lemma for cycsubmcom and cygabl . Formerly part of proof for cygabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 20-Jan-2024)

Ref Expression
Hypotheses cyccom.c ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐶 ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) )
cyccom.d ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑛 ∈ 𝑍 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
cyccom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
cyccom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐶 )
cyccom.z ⊢ ( 𝜑 → 𝑍 ⊆ ℂ )
Assertion cyccom ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cyccom.c ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐶 ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) )
2 cyccom.d ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑛 ∈ 𝑍 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
3 cyccom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
4 cyccom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐶 )
5 cyccom.z ⊢ ( 𝜑 → 𝑍 ⊆ ℂ )
6 eqeq1 ⊢ ( 𝑐 = 𝑌 → ( 𝑐 = ( 𝑥 · 𝐴 ) ↔ 𝑌 = ( 𝑥 · 𝐴 ) ) )
7 6 rexbidv ⊢ ( 𝑐 = 𝑌 → ( ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) ) )
8 7 rspccv ⊢ ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) → ( 𝑌 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) ) )
9 1 8 syl ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) ) )
10 eqeq1 ⊢ ( 𝑐 = 𝑋 → ( 𝑐 = ( 𝑥 · 𝐴 ) ↔ 𝑋 = ( 𝑥 · 𝐴 ) ) )
11 10 rexbidv ⊢ ( 𝑐 = 𝑋 → ( ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) ) )
12 11 rspccv ⊢ ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑥 ∈ 𝑍 𝑐 = ( 𝑥 · 𝐴 ) → ( 𝑋 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) ) )
13 1 12 syl ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) ) )
14 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
15 14 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑌 = ( 𝑥 · 𝐴 ) ↔ 𝑌 = ( 𝑦 · 𝐴 ) ) )
16 15 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑍 𝑌 = ( 𝑦 · 𝐴 ) )
17 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑍 ∃ 𝑦 ∈ 𝑍 ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) ↔ ( ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑍 𝑌 = ( 𝑦 · 𝐴 ) ) )
18 5 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ℂ ) )
19 18 com12 ⊢ ( 𝑥 ∈ 𝑍 → ( 𝜑 → 𝑥 ∈ ℂ ) )
20 19 adantr ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) → ( 𝜑 → 𝑥 ∈ ℂ ) )
21 20 impcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → 𝑥 ∈ ℂ )
22 5 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑍 → 𝑦 ∈ ℂ ) )
23 22 a1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 → ( 𝑦 ∈ 𝑍 → 𝑦 ∈ ℂ ) ) )
24 23 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → 𝑦 ∈ ℂ )
25 21 24 addcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
26 25 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐴 ) = ( ( 𝑦 + 𝑥 ) · 𝐴 ) )
27 simpr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) )
28 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ∀ 𝑚 ∈ 𝑍 ∀ 𝑛 ∈ 𝑍 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
29 oveq1 ⊢ ( 𝑚 = 𝑥 → ( 𝑚 + 𝑛 ) = ( 𝑥 + 𝑛 ) )
30 29 oveq1d ⊢ ( 𝑚 = 𝑥 → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑥 + 𝑛 ) · 𝐴 ) )
31 oveq1 ⊢ ( 𝑚 = 𝑥 → ( 𝑚 · 𝐴 ) = ( 𝑥 · 𝐴 ) )
32 31 oveq1d ⊢ ( 𝑚 = 𝑥 → ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) = ( ( 𝑥 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
33 30 32 eqeq12d ⊢ ( 𝑚 = 𝑥 → ( ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ↔ ( ( 𝑥 + 𝑛 ) · 𝐴 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ) )
34 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑥 + 𝑛 ) = ( 𝑥 + 𝑦 ) )
35 34 oveq1d ⊢ ( 𝑛 = 𝑦 → ( ( 𝑥 + 𝑛 ) · 𝐴 ) = ( ( 𝑥 + 𝑦 ) · 𝐴 ) )
36 oveq1 ⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
37 36 oveq2d ⊢ ( 𝑛 = 𝑦 → ( ( 𝑥 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) = ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) )
38 35 37 eqeq12d ⊢ ( 𝑛 = 𝑦 → ( ( ( 𝑥 + 𝑛 ) · 𝐴 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ↔ ( ( 𝑥 + 𝑦 ) · 𝐴 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) ) )
39 33 38 rspc2va ⊢ ( ( ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑛 ∈ 𝑍 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ) → ( ( 𝑥 + 𝑦 ) · 𝐴 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) )
40 27 28 39 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐴 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) )
41 27 ancomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( 𝑦 ∈ 𝑍 ∧ 𝑥 ∈ 𝑍 ) )
42 oveq1 ⊢ ( 𝑚 = 𝑦 → ( 𝑚 + 𝑛 ) = ( 𝑦 + 𝑛 ) )
43 42 oveq1d ⊢ ( 𝑚 = 𝑦 → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑦 + 𝑛 ) · 𝐴 ) )
44 oveq1 ⊢ ( 𝑚 = 𝑦 → ( 𝑚 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
45 44 oveq1d ⊢ ( 𝑚 = 𝑦 → ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) = ( ( 𝑦 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
46 43 45 eqeq12d ⊢ ( 𝑚 = 𝑦 → ( ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ↔ ( ( 𝑦 + 𝑛 ) · 𝐴 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ) )
47 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑦 + 𝑛 ) = ( 𝑦 + 𝑥 ) )
48 47 oveq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑦 + 𝑛 ) · 𝐴 ) = ( ( 𝑦 + 𝑥 ) · 𝐴 ) )
49 oveq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 𝐴 ) = ( 𝑥 · 𝐴 ) )
50 49 oveq2d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑦 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
51 48 50 eqeq12d ⊢ ( 𝑛 = 𝑥 → ( ( ( 𝑦 + 𝑛 ) · 𝐴 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ↔ ( ( 𝑦 + 𝑥 ) · 𝐴 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) ) )
52 46 51 rspc2va ⊢ ( ( ( 𝑦 ∈ 𝑍 ∧ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑛 ∈ 𝑍 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) ) → ( ( 𝑦 + 𝑥 ) · 𝐴 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
53 41 28 52 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( ( 𝑦 + 𝑥 ) · 𝐴 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
54 26 40 53 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
55 oveq12 ⊢ ( ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) )
56 oveq12 ⊢ ( ( 𝑌 = ( 𝑦 · 𝐴 ) ∧ 𝑋 = ( 𝑥 · 𝐴 ) ) → ( 𝑌 + 𝑋 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
57 56 ancoms ⊢ ( ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) → ( 𝑌 + 𝑋 ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) )
58 55 57 eqeq12d ⊢ ( ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ↔ ( ( 𝑥 · 𝐴 ) + ( 𝑦 · 𝐴 ) ) = ( ( 𝑦 · 𝐴 ) + ( 𝑥 · 𝐴 ) ) ) )
59 54 58 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ 𝑍 ) ) → ( ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
60 59 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑍 ∃ 𝑦 ∈ 𝑍 ( 𝑋 = ( 𝑥 · 𝐴 ) ∧ 𝑌 = ( 𝑦 · 𝐴 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
61 17 60 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑍 𝑌 = ( 𝑦 · 𝐴 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
62 61 expd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) → ( ∃ 𝑦 ∈ 𝑍 𝑌 = ( 𝑦 · 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )
63 16 62 syl7bi ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑍 𝑋 = ( 𝑥 · 𝐴 ) → ( ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )
64 13 63 syld ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )
65 64 com23 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑍 𝑌 = ( 𝑥 · 𝐴 ) → ( 𝑋 ∈ 𝐶 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )
66 9 65 syld ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐶 → ( 𝑋 ∈ 𝐶 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )
67 4 3 66 mp2d ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )