rglcom4d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rglcom4d		Structured version Visualization version GIF version

Theorem rglcom4d 19994

Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom 20056 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.)

**Hypotheses**
Ref	Expression
o2timesd.e	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
o2timesd.u	⊢ (𝜑 → 1 ∈ 𝐵)
o2timesd.i	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥)
o2timesd.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
rglcom4d.a	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵)
rglcom4d.d	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
rglcom4d.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
rglcom4d	⊢ (𝜑 → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))

Distinct variable groups: 𝑥,𝐵,𝑦,𝑧 𝑥,𝑋,𝑦,𝑧 𝑥, 1 ,𝑦,𝑧 𝑥, · ,𝑦,𝑧 𝑥, + ,𝑦,𝑧 𝑥,𝑌,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧)

**Proof of Theorem rglcom4d**
Step	Hyp	Ref	Expression
1		o2timesd.u	. . . . . . 7 ⊢ (𝜑 → 1 ∈ 𝐵)
2	1, 1	jca 512	. . . . . 6 ⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵))
3		rglcom4d.a	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵)
4		oveq1 7401	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 + 𝑦) = ( 1 + 𝑦))
5	4	eleq1d 2818	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ ( 1 + 𝑦) ∈ 𝐵))
6		oveq2 7402	. . . . . . . 8 ⊢ (𝑦 = 1 → ( 1 + 𝑦) = ( 1 + 1 ))
7	6	eleq1d 2818	. . . . . . 7 ⊢ (𝑦 = 1 → (( 1 + 𝑦) ∈ 𝐵 ↔ ( 1 + 1 ) ∈ 𝐵))
8	5, 7	rspc2v 3619	. . . . . 6 ⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵 → ( 1 + 1 ) ∈ 𝐵))
9	2, 3, 8	sylc 65	. . . . 5 ⊢ (𝜑 → ( 1 + 1 ) ∈ 𝐵)
10		o2timesd.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
11		rglcom4d.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
12	9, 10, 11	3jca 1128	. . . 4 ⊢ (𝜑 → (( 1 + 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
13		rglcom4d.d	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
14		oveq1 7401	. . . . . 6 ⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑦 + 𝑧)))
15		oveq1 7401	. . . . . . 7 ⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑦) = (( 1 + 1 ) · 𝑦))
16		oveq1 7401	. . . . . . 7 ⊢ (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑧) = (( 1 + 1 ) · 𝑧))
17	15, 16	oveq12d 7412	. . . . . 6 ⊢ (𝑥 = ( 1 + 1 ) → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)))
18	14, 17	eqeq12d 2748	. . . . 5 ⊢ (𝑥 = ( 1 + 1 ) → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧))))
19		oveq1 7401	. . . . . . 7 ⊢ (𝑦 = 𝑋 → (𝑦 + 𝑧) = (𝑋 + 𝑧))
20	19	oveq2d 7410	. . . . . 6 ⊢ (𝑦 = 𝑋 → (( 1 + 1 ) · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑧)))
21		oveq2 7402	. . . . . . 7 ⊢ (𝑦 = 𝑋 → (( 1 + 1 ) · 𝑦) = (( 1 + 1 ) · 𝑋))
22	21	oveq1d 7409	. . . . . 6 ⊢ (𝑦 = 𝑋 → ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)))
23	20, 22	eqeq12d 2748	. . . . 5 ⊢ (𝑦 = 𝑋 → ((( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧))))
24		oveq2 7402	. . . . . . 7 ⊢ (𝑧 = 𝑌 → (𝑋 + 𝑧) = (𝑋 + 𝑌))
25	24	oveq2d 7410	. . . . . 6 ⊢ (𝑧 = 𝑌 → (( 1 + 1 ) · (𝑋 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑌)))
26		oveq2 7402	. . . . . . 7 ⊢ (𝑧 = 𝑌 → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · 𝑌))
27	26	oveq2d 7410	. . . . . 6 ⊢ (𝑧 = 𝑌 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))
28	25, 27	eqeq12d 2748	. . . . 5 ⊢ (𝑧 = 𝑌 → ((( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))))
29	18, 23, 28	rspc3v 3624	. . . 4 ⊢ ((( 1 + 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))))
30	12, 13, 29	sylc 65	. . 3 ⊢ (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))
31		oveq1 7401	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
32	31	eleq1d 2818	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
33		oveq2 7402	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
34	33	eleq1d 2818	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
35	32, 34	rspc2va 3620	. . . . . 6 ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
36	10, 11, 3, 35	syl21anc 836	. . . . 5 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
37	1, 1, 36	3jca 1128	. . . 4 ⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵))
38		o2timesd.e	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
39	4	oveq1d 7409	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 + 𝑦) · 𝑧) = (( 1 + 𝑦) · 𝑧))
40		oveq1 7401	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 · 𝑧) = ( 1 · 𝑧))
41	40	oveq1d 7409	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + (𝑦 · 𝑧)))
42	39, 41	eqeq12d 2748	. . . . 5 ⊢ (𝑥 = 1 → (((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧))))
43	6	oveq1d 7409	. . . . . 6 ⊢ (𝑦 = 1 → (( 1 + 𝑦) · 𝑧) = (( 1 + 1 ) · 𝑧))
44		oveq1 7401	. . . . . . 7 ⊢ (𝑦 = 1 → (𝑦 · 𝑧) = ( 1 · 𝑧))
45	44	oveq2d 7410	. . . . . 6 ⊢ (𝑦 = 1 → (( 1 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + ( 1 · 𝑧)))
46	43, 45	eqeq12d 2748	. . . . 5 ⊢ (𝑦 = 1 → ((( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧))))
47		oveq2 7402	. . . . . 6 ⊢ (𝑧 = (𝑋 + 𝑌) → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · (𝑋 + 𝑌)))
48		oveq2 7402	. . . . . . 7 ⊢ (𝑧 = (𝑋 + 𝑌) → ( 1 · 𝑧) = ( 1 · (𝑋 + 𝑌)))
49	48, 48	oveq12d 7412	. . . . . 6 ⊢ (𝑧 = (𝑋 + 𝑌) → (( 1 · 𝑧) + ( 1 · 𝑧)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
50	47, 49	eqeq12d 2748	. . . . 5 ⊢ (𝑧 = (𝑋 + 𝑌) → ((( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))))
51	42, 46, 50	rspc3v 3624	. . . 4 ⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))))
52	37, 38, 51	sylc 65	. . 3 ⊢ (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
53	30, 52	eqtr3d 2774	. 2 ⊢ (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
54		o2timesd.i	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥)
55	38, 1, 54, 10	o2timesd 19993	. . . 4 ⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 + 1 ) · 𝑋))
56	55	eqcomd 2738	. . 3 ⊢ (𝜑 → (( 1 + 1 ) · 𝑋) = (𝑋 + 𝑋))
57	38, 1, 54, 11	o2timesd 19993	. . . 4 ⊢ (𝜑 → (𝑌 + 𝑌) = (( 1 + 1 ) · 𝑌))
58	57	eqcomd 2738	. . 3 ⊢ (𝜑 → (( 1 + 1 ) · 𝑌) = (𝑌 + 𝑌))
59	56, 58	oveq12d 7412	. 2 ⊢ (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = ((𝑋 + 𝑋) + (𝑌 + 𝑌)))
60		oveq2 7402	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → ( 1 · 𝑥) = ( 1 · (𝑋 + 𝑌)))
61		id 22	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → 𝑥 = (𝑋 + 𝑌))
62	60, 61	eqeq12d 2748	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌)))
63	62	rspcva 3608	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌))
64	36, 54, 63	syl2anc 584	. . 3 ⊢ (𝜑 → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌))
65	64, 64	oveq12d 7412	. 2 ⊢ (𝜑 → (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))
66	53, 59, 65	3eqtr3d 2780	1 ⊢ (𝜑 → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 (class class class)co 7394

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rab 3433 df-v 3476 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5143 df-iota 6485 df-fv 6541 df-ov 7397

This theorem is referenced by: srgcom4lem 19996 ringcomlem 20055

W3C validator