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 
|- ( ph -> A. c e. C E. x e. Z c = ( x .x. A ) )
cyccom.d 
|- ( ph -> A. m e. Z A. n e. Z ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
cyccom.x 
|- ( ph -> X e. C )
cyccom.y 
|- ( ph -> Y e. C )
cyccom.z 
|- ( ph -> Z C_ CC )
Assertion cyccom 
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )

Proof

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