Metamath Proof Explorer

Theorem srgcom4

Description: Restricted commutativity of the addition in semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by AV, 1-Feb-2025) (Proof modification is discouraged.)

Ref Expression
Hypotheses srgcom4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srgcom4.p ⊢ + = ( +g ‘ 𝑅 )
Assertion srgcom4 ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) + 𝑌 ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 srgcom4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srgcom4.p ⊢ + = ( +g ‘ 𝑅 )
3 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
4 3 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Mnd )
5 simp2 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
6 simp3 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
7 1 2 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
8 4 5 5 6 7 syl13anc ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + 𝑌 ) = ( 𝑋 + ( 𝑋 + 𝑌 ) ) )
9 8 eqcomd ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑋 + 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + 𝑌 ) )
10 9 oveq1d ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) + 𝑌 ) = ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) )
11 1 2 srgacl ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
12 5 11 syld3an3 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑋 ) ∈ 𝐵 )
13 1 2 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( 𝑋 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
14 4 12 6 6 13 syl13anc ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 + 𝑋 ) + 𝑌 ) + 𝑌 ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
15 1 2 srgcom4lem ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
16 1 2 srgacl ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
17 1 2 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑋 + 𝑌 ) ) ) )
18 4 5 6 16 17 syl13anc ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑋 + 𝑌 ) ) ) )
19 1 2 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑌 ) = ( 𝑌 + ( 𝑋 + 𝑌 ) ) )
20 19 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑌 + ( 𝑋 + 𝑌 ) ) = ( ( 𝑌 + 𝑋 ) + 𝑌 ) )
21 4 6 5 6 20 syl13anc ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + ( 𝑋 + 𝑌 ) ) = ( ( 𝑌 + 𝑋 ) + 𝑌 ) )
22 21 oveq2d ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 + ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + ( ( 𝑌 + 𝑋 ) + 𝑌 ) ) )
23 1 2 srgacl ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
24 23 3com23 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
25 1 2 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) = ( 𝑋 + ( ( 𝑌 + 𝑋 ) + 𝑌 ) ) )
26 25 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 + ( ( 𝑌 + 𝑋 ) + 𝑌 ) ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )
27 4 5 24 6 26 syl13anc ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( ( 𝑌 + 𝑋 ) + 𝑌 ) ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )
28 22 27 eqtrd ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + ( 𝑌 + ( 𝑋 + 𝑌 ) ) ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )
29 15 18 28 3eqtrd ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )
30 10 14 29 3eqtrd ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + ( 𝑋 + 𝑌 ) ) + 𝑌 ) = ( ( 𝑋 + ( 𝑌 + 𝑋 ) ) + 𝑌 ) )