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 φ c C x Z c = x · ˙ A
cyccom.d φ m Z n Z m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
cyccom.x φ X C
cyccom.y φ Y C
cyccom.z φ Z
Assertion cyccom φ X + ˙ Y = Y + ˙ X

Proof

Step Hyp Ref Expression
1 cyccom.c φ c C x Z c = x · ˙ A
2 cyccom.d φ m Z n Z m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
3 cyccom.x φ X C
4 cyccom.y φ Y C
5 cyccom.z φ Z
6 eqeq1 c = Y c = x · ˙ A Y = x · ˙ A
7 6 rexbidv c = Y x Z c = x · ˙ A x Z Y = x · ˙ A
8 7 rspccv c C x Z c = x · ˙ A Y C x Z Y = x · ˙ A
9 1 8 syl φ Y C x Z Y = x · ˙ A
10 eqeq1 c = X c = x · ˙ A X = x · ˙ A
11 10 rexbidv c = X x Z c = x · ˙ A x Z X = x · ˙ A
12 11 rspccv c C x Z c = x · ˙ A X C x Z X = x · ˙ A
13 1 12 syl φ X C x Z X = x · ˙ A
14 oveq1 x = y x · ˙ A = y · ˙ A
15 14 eqeq2d x = y Y = x · ˙ A Y = y · ˙ A
16 15 cbvrexvw x Z Y = x · ˙ A y Z Y = y · ˙ A
17 reeanv x Z y Z X = x · ˙ A Y = y · ˙ A x Z X = x · ˙ A y Z Y = y · ˙ A
18 5 sseld φ x Z x
19 18 com12 x Z φ x
20 19 adantr x Z y Z φ x
21 20 impcom φ x Z y Z x
22 5 sseld φ y Z y
23 22 a1d φ x Z y Z y
24 23 imp32 φ x Z y Z y
25 21 24 addcomd φ x Z y Z x + y = y + x
26 25 oveq1d φ x Z y Z x + y · ˙ A = y + x · ˙ A
27 simpr φ x Z y Z x Z y Z
28 2 adantr φ x Z y Z m Z n Z m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
29 oveq1 m = x m + n = x + n
30 29 oveq1d m = x m + n · ˙ A = x + n · ˙ A
31 oveq1 m = x m · ˙ A = x · ˙ A
32 31 oveq1d m = x m · ˙ A + ˙ n · ˙ A = x · ˙ A + ˙ n · ˙ A
33 30 32 eqeq12d m = x m + n · ˙ A = m · ˙ A + ˙ n · ˙ A x + n · ˙ A = x · ˙ A + ˙ n · ˙ A
34 oveq2 n = y x + n = x + y
35 34 oveq1d n = y x + n · ˙ A = x + y · ˙ A
36 oveq1 n = y n · ˙ A = y · ˙ A
37 36 oveq2d n = y x · ˙ A + ˙ n · ˙ A = x · ˙ A + ˙ y · ˙ A
38 35 37 eqeq12d n = y x + n · ˙ A = x · ˙ A + ˙ n · ˙ A x + y · ˙ A = x · ˙ A + ˙ y · ˙ A
39 33 38 rspc2va x Z y Z m Z n Z m + n · ˙ A = m · ˙ A + ˙ n · ˙ A x + y · ˙ A = x · ˙ A + ˙ y · ˙ A
40 27 28 39 syl2anc φ x Z y Z x + y · ˙ A = x · ˙ A + ˙ y · ˙ A
41 27 ancomd φ x Z y Z y Z x Z
42 oveq1 m = y m + n = y + n
43 42 oveq1d m = y m + n · ˙ A = y + n · ˙ A
44 oveq1 m = y m · ˙ A = y · ˙ A
45 44 oveq1d m = y m · ˙ A + ˙ n · ˙ A = y · ˙ A + ˙ n · ˙ A
46 43 45 eqeq12d m = y m + n · ˙ A = m · ˙ A + ˙ n · ˙ A y + n · ˙ A = y · ˙ A + ˙ n · ˙ A
47 oveq2 n = x y + n = y + x
48 47 oveq1d n = x y + n · ˙ A = y + x · ˙ A
49 oveq1 n = x n · ˙ A = x · ˙ A
50 49 oveq2d n = x y · ˙ A + ˙ n · ˙ A = y · ˙ A + ˙ x · ˙ A
51 48 50 eqeq12d n = x y + n · ˙ A = y · ˙ A + ˙ n · ˙ A y + x · ˙ A = y · ˙ A + ˙ x · ˙ A
52 46 51 rspc2va y Z x Z m Z n Z m + n · ˙ A = m · ˙ A + ˙ n · ˙ A y + x · ˙ A = y · ˙ A + ˙ x · ˙ A
53 41 28 52 syl2anc φ x Z y Z y + x · ˙ A = y · ˙ A + ˙ x · ˙ A
54 26 40 53 3eqtr3d φ x Z y Z x · ˙ A + ˙ y · ˙ A = y · ˙ A + ˙ x · ˙ A
55 oveq12 X = x · ˙ A Y = y · ˙ A X + ˙ Y = x · ˙ A + ˙ y · ˙ A
56 oveq12 Y = y · ˙ A X = x · ˙ A Y + ˙ X = y · ˙ A + ˙ x · ˙ A
57 56 ancoms X = x · ˙ A Y = y · ˙ A Y + ˙ X = y · ˙ A + ˙ x · ˙ A
58 55 57 eqeq12d X = x · ˙ A Y = y · ˙ A X + ˙ Y = Y + ˙ X x · ˙ A + ˙ y · ˙ A = y · ˙ A + ˙ x · ˙ A
59 54 58 syl5ibrcom φ x Z y Z X = x · ˙ A Y = y · ˙ A X + ˙ Y = Y + ˙ X
60 59 rexlimdvva φ x Z y Z X = x · ˙ A Y = y · ˙ A X + ˙ Y = Y + ˙ X
61 17 60 syl5bir φ x Z X = x · ˙ A y Z Y = y · ˙ A X + ˙ Y = Y + ˙ X
62 61 expd φ x Z X = x · ˙ A y Z Y = y · ˙ A X + ˙ Y = Y + ˙ X
63 16 62 syl7bi φ x Z X = x · ˙ A x Z Y = x · ˙ A X + ˙ Y = Y + ˙ X
64 13 63 syld φ X C x Z Y = x · ˙ A X + ˙ Y = Y + ˙ X
65 64 com23 φ x Z Y = x · ˙ A X C X + ˙ Y = Y + ˙ X
66 9 65 syld φ Y C X C X + ˙ Y = Y + ˙ X
67 4 3 66 mp2d φ X + ˙ Y = Y + ˙ X