Metamath Proof Explorer

Theorem rglcom4d

Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom depends on the closure of the addition, the (left and right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025)

Ref Expression
Hypotheses o2timesd.e 
|- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
o2timesd.u 
|- ( ph -> .1. e. B )
o2timesd.i 
|- ( ph -> A. x e. B ( .1. .x. x ) = x )
o2timesd.x 
|- ( ph -> X e. B )
rglcom4d.a 
|- ( ph -> A. x e. B A. y e. B ( x .+ y ) e. B )
rglcom4d.d 
|- ( ph -> A. x e. B A. y e. B A. z e. B ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
rglcom4d.y 
|- ( ph -> Y e. B )
Assertion rglcom4d 
|- ( ph -> ( ( X .+ X ) .+ ( Y .+ Y ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )

Proof

Step Hyp Ref Expression
1 o2timesd.e 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
2 o2timesd.u 
 |-  ( ph -> .1. e. B )
3 o2timesd.i 
 |-  ( ph -> A. x e. B ( .1. .x. x ) = x )
4 o2timesd.x 
 |-  ( ph -> X e. B )
5 rglcom4d.a 
 |-  ( ph -> A. x e. B A. y e. B ( x .+ y ) e. B )
6 rglcom4d.d 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
7 rglcom4d.y 
 |-  ( ph -> Y e. B )
8 2 2 jca 
 |-  ( ph -> ( .1. e. B /\ .1. e. B ) )
9 oveq1 
 |-  ( x = .1. -> ( x .+ y ) = ( .1. .+ y ) )
10 9 eleq1d 
 |-  ( x = .1. -> ( ( x .+ y ) e. B <-> ( .1. .+ y ) e. B ) )
11 oveq2 
 |-  ( y = .1. -> ( .1. .+ y ) = ( .1. .+ .1. ) )
12 11 eleq1d 
 |-  ( y = .1. -> ( ( .1. .+ y ) e. B <-> ( .1. .+ .1. ) e. B ) )
13 10 12 rspc2v 
 |-  ( ( .1. e. B /\ .1. e. B ) -> ( A. x e. B A. y e. B ( x .+ y ) e. B -> ( .1. .+ .1. ) e. B ) )
14 8 5 13 sylc 
 |-  ( ph -> ( .1. .+ .1. ) e. B )
15 14 4 7 3jca 
 |-  ( ph -> ( ( .1. .+ .1. ) e. B /\ X e. B /\ Y e. B ) )
16 oveq1 
 |-  ( x = ( .1. .+ .1. ) -> ( x .x. ( y .+ z ) ) = ( ( .1. .+ .1. ) .x. ( y .+ z ) ) )
17 oveq1 
 |-  ( x = ( .1. .+ .1. ) -> ( x .x. y ) = ( ( .1. .+ .1. ) .x. y ) )
18 oveq1 
 |-  ( x = ( .1. .+ .1. ) -> ( x .x. z ) = ( ( .1. .+ .1. ) .x. z ) )
19 17 18 oveq12d 
 |-  ( x = ( .1. .+ .1. ) -> ( ( x .x. y ) .+ ( x .x. z ) ) = ( ( ( .1. .+ .1. ) .x. y ) .+ ( ( .1. .+ .1. ) .x. z ) ) )
20 16 19 eqeq12d 
 |-  ( x = ( .1. .+ .1. ) -> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) <-> ( ( .1. .+ .1. ) .x. ( y .+ z ) ) = ( ( ( .1. .+ .1. ) .x. y ) .+ ( ( .1. .+ .1. ) .x. z ) ) ) )
21 oveq1 
 |-  ( y = X -> ( y .+ z ) = ( X .+ z ) )
22 21 oveq2d 
 |-  ( y = X -> ( ( .1. .+ .1. ) .x. ( y .+ z ) ) = ( ( .1. .+ .1. ) .x. ( X .+ z ) ) )
23 oveq2 
 |-  ( y = X -> ( ( .1. .+ .1. ) .x. y ) = ( ( .1. .+ .1. ) .x. X ) )
24 23 oveq1d 
 |-  ( y = X -> ( ( ( .1. .+ .1. ) .x. y ) .+ ( ( .1. .+ .1. ) .x. z ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. z ) ) )
25 22 24 eqeq12d 
 |-  ( y = X -> ( ( ( .1. .+ .1. ) .x. ( y .+ z ) ) = ( ( ( .1. .+ .1. ) .x. y ) .+ ( ( .1. .+ .1. ) .x. z ) ) <-> ( ( .1. .+ .1. ) .x. ( X .+ z ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. z ) ) ) )
26 oveq2 
 |-  ( z = Y -> ( X .+ z ) = ( X .+ Y ) )
27 26 oveq2d 
 |-  ( z = Y -> ( ( .1. .+ .1. ) .x. ( X .+ z ) ) = ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) )
28 oveq2 
 |-  ( z = Y -> ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .+ .1. ) .x. Y ) )
29 28 oveq2d 
 |-  ( z = Y -> ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. z ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) )
30 27 29 eqeq12d 
 |-  ( z = Y -> ( ( ( .1. .+ .1. ) .x. ( X .+ z ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. z ) ) <-> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) ) )
31 20 25 30 rspc3v 
 |-  ( ( ( .1. .+ .1. ) e. B /\ X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B A. z e. B ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) ) )
32 15 6 31 sylc 
 |-  ( ph -> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) )
33 oveq1 
 |-  ( x = X -> ( x .+ y ) = ( X .+ y ) )
34 33 eleq1d 
 |-  ( x = X -> ( ( x .+ y ) e. B <-> ( X .+ y ) e. B ) )
35 oveq2 
 |-  ( y = Y -> ( X .+ y ) = ( X .+ Y ) )
36 35 eleq1d 
 |-  ( y = Y -> ( ( X .+ y ) e. B <-> ( X .+ Y ) e. B ) )
37 34 36 rspc2va 
 |-  ( ( ( X e. B /\ Y e. B ) /\ A. x e. B A. y e. B ( x .+ y ) e. B ) -> ( X .+ Y ) e. B )
38 4 7 5 37 syl21anc 
 |-  ( ph -> ( X .+ Y ) e. B )
39 2 2 38 3jca 
 |-  ( ph -> ( .1. e. B /\ .1. e. B /\ ( X .+ Y ) e. B ) )
40 9 oveq1d 
 |-  ( x = .1. -> ( ( x .+ y ) .x. z ) = ( ( .1. .+ y ) .x. z ) )
41 oveq1 
 |-  ( x = .1. -> ( x .x. z ) = ( .1. .x. z ) )
42 41 oveq1d 
 |-  ( x = .1. -> ( ( x .x. z ) .+ ( y .x. z ) ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) )
43 40 42 eqeq12d 
 |-  ( x = .1. -> ( ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) <-> ( ( .1. .+ y ) .x. z ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) ) )
44 11 oveq1d 
 |-  ( y = .1. -> ( ( .1. .+ y ) .x. z ) = ( ( .1. .+ .1. ) .x. z ) )
45 oveq1 
 |-  ( y = .1. -> ( y .x. z ) = ( .1. .x. z ) )
46 45 oveq2d 
 |-  ( y = .1. -> ( ( .1. .x. z ) .+ ( y .x. z ) ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) )
47 44 46 eqeq12d 
 |-  ( y = .1. -> ( ( ( .1. .+ y ) .x. z ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) <-> ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) ) )
48 oveq2 
 |-  ( z = ( X .+ Y ) -> ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) )
49 oveq2 
 |-  ( z = ( X .+ Y ) -> ( .1. .x. z ) = ( .1. .x. ( X .+ Y ) ) )
50 49 49 oveq12d 
 |-  ( z = ( X .+ Y ) -> ( ( .1. .x. z ) .+ ( .1. .x. z ) ) = ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) )
51 48 50 eqeq12d 
 |-  ( z = ( X .+ Y ) -> ( ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) <-> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) ) )
52 43 47 51 rspc3v 
 |-  ( ( .1. e. B /\ .1. e. B /\ ( X .+ Y ) e. B ) -> ( A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) ) )
53 39 1 52 sylc 
 |-  ( ph -> ( ( .1. .+ .1. ) .x. ( X .+ Y ) ) = ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) )
54 32 53 eqtr3d 
 |-  ( ph -> ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) = ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) )
55 1 2 3 4 o2timesd 
 |-  ( ph -> ( X .+ X ) = ( ( .1. .+ .1. ) .x. X ) )
56 55 eqcomd 
 |-  ( ph -> ( ( .1. .+ .1. ) .x. X ) = ( X .+ X ) )
57 1 2 3 7 o2timesd 
 |-  ( ph -> ( Y .+ Y ) = ( ( .1. .+ .1. ) .x. Y ) )
58 57 eqcomd 
 |-  ( ph -> ( ( .1. .+ .1. ) .x. Y ) = ( Y .+ Y ) )
59 56 58 oveq12d 
 |-  ( ph -> ( ( ( .1. .+ .1. ) .x. X ) .+ ( ( .1. .+ .1. ) .x. Y ) ) = ( ( X .+ X ) .+ ( Y .+ Y ) ) )
60 oveq2 
 |-  ( x = ( X .+ Y ) -> ( .1. .x. x ) = ( .1. .x. ( X .+ Y ) ) )
61 id 
 |-  ( x = ( X .+ Y ) -> x = ( X .+ Y ) )
62 60 61 eqeq12d 
 |-  ( x = ( X .+ Y ) -> ( ( .1. .x. x ) = x <-> ( .1. .x. ( X .+ Y ) ) = ( X .+ Y ) ) )
63 62 rspcva 
 |-  ( ( ( X .+ Y ) e. B /\ A. x e. B ( .1. .x. x ) = x ) -> ( .1. .x. ( X .+ Y ) ) = ( X .+ Y ) )
64 38 3 63 syl2anc 
 |-  ( ph -> ( .1. .x. ( X .+ Y ) ) = ( X .+ Y ) )
65 64 64 oveq12d 
 |-  ( ph -> ( ( .1. .x. ( X .+ Y ) ) .+ ( .1. .x. ( X .+ Y ) ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )
66 54 59 65 3eqtr3d 
 |-  ( ph -> ( ( X .+ X ) .+ ( Y .+ Y ) ) = ( ( X .+ Y ) .+ ( X .+ Y ) ) )