This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem srgcom4lem

Description: Lemma for srgcom4 . This (formerly) part of the proof for ringcom is applicable for semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 srgcom4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srgcom4.p ⊢ + = ( +g ‘ 𝑅 )
3 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
4 1 2 3 srgdir ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
5 4 ralrimivvva ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) + ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 1 7 srgidcl ⊢ ( 𝑅 ∈ SRing → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
9 8 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
10 1 3 7 srglidm ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
11 10 ralrimiva ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
12 11 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
13 simp2 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14 1 2 srgacl ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
15 14 3expb ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
16 15 ralrimivva ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 )
17 16 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 )
18 1 2 3 srgdi ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) + ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) )
19 18 ralrimivvva ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) + ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) + ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) )
21 simp3 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
22 6 9 12 13 17 20 21 rglcom4d ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )