isring - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > isring		GIF version

Theorem isring 13183

Description: The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)

**Hypotheses**
Ref	Expression
isring.b	⊢ 𝐵 = (Base‘𝑅)
isring.g	⊢ 𝐺 = (mulGrp‘𝑅)
isring.p	⊢ + = (+_g‘𝑅)
isring.t	⊢ · = (._r‘𝑅)

**Assertion**
Ref	Expression
isring	⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))

Distinct variable groups: 𝑥,𝑦,𝑧,𝐵 𝑥, + ,𝑦,𝑧 𝑥,𝑅,𝑦,𝑧 𝑥, · ,𝑦,𝑧 Allowed substitution hints: 𝐺(𝑥,𝑦,𝑧)

Proof of Theorem isring Dummy variables 𝑝 𝑏 𝑟 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5516	. . . . . 6 ⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅))
2		isring.g	. . . . . 6 ⊢ 𝐺 = (mulGrp‘𝑅)
3	1, 2	eqtr4di 2228	. . . . 5 ⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = 𝐺)
4	3	eleq1d 2246	. . . 4 ⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ Mnd ↔ 𝐺 ∈ Mnd))
5		basfn 12520	. . . . . . 7 ⊢ Base Fn V
6		vex 2741	. . . . . . 7 ⊢ 𝑟 ∈ V
7		funfvex 5533	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
8	7	funfni 5317	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
9	5, 6, 8	mp2an 426	. . . . . 6 ⊢ (Base‘𝑟) ∈ V
10	9	a1i 9	. . . . 5 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
11		fveq2 5516	. . . . . 6 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
12		isring.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
13	11, 12	eqtr4di 2228	. . . . 5 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
14		plusgslid 12571	. . . . . . . . 9 ⊢ (+_g = Slot (+_g‘ndx) ∧ (+_g‘ndx) ∈ ℕ)
15	14	slotex 12489	. . . . . . . 8 ⊢ (𝑟 ∈ V → (+_g‘𝑟) ∈ V)
16	15	elv 2742	. . . . . . 7 ⊢ (+_g‘𝑟) ∈ V
17	16	a1i 9	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+_g‘𝑟) ∈ V)
18		simpl 109	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅)
19	18	fveq2d 5520	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+_g‘𝑟) = (+_g‘𝑅))
20		isring.p	. . . . . . 7 ⊢ + = (+_g‘𝑅)
21	19, 20	eqtr4di 2228	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (+_g‘𝑟) = + )
22		mulrslid 12590	. . . . . . . . . 10 ⊢ (._r = Slot (._r‘ndx) ∧ (._r‘ndx) ∈ ℕ)
23	22	slotex 12489	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (._r‘𝑟) ∈ V)
24	23	elv 2742	. . . . . . . 8 ⊢ (._r‘𝑟) ∈ V
25	24	a1i 9	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → (._r‘𝑟) ∈ V)
26		simpll 527	. . . . . . . . 9 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → 𝑟 = 𝑅)
27	26	fveq2d 5520	. . . . . . . 8 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → (._r‘𝑟) = (._r‘𝑅))
28		isring.t	. . . . . . . 8 ⊢ · = (._r‘𝑅)
29	27, 28	eqtr4di 2228	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → (._r‘𝑟) = · )
30		simpllr 534	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵)
31		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · )
32		eqidd 2178	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥)
33		simplr 528	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + )
34	33	oveqd 5892	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧))
35	31, 32, 34	oveq123d 5896	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧)))
36	31	oveqd 5892	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦))
37	31	oveqd 5892	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧))
38	33, 36, 37	oveq123d 5896	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
39	35, 38	eqeq12d 2192	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))))
40	33	oveqd 5892	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦))
41		eqidd 2178	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧)
42	31, 40, 41	oveq123d 5896	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧))
43	31	oveqd 5892	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧))
44	33, 37, 43	oveq123d 5896	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
45	42, 44	eqeq12d 2192	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))
46	39, 45	anbi12d 473	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
47	30, 46	raleqbidv 2685	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
48	30, 47	raleqbidv 2685	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
49	30, 48	raleqbidv 2685	. . . . . . 7 ⊢ ((((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
50	25, 29, 49	sbcied2 3001	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑝 = + ) → ([(._r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
51	17, 21, 50	sbcied2 3001	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(+_g‘𝑟) / 𝑝][(._r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
52	10, 13, 51	sbcied2 3001	. . . 4 ⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+_g‘𝑟) / 𝑝][(._r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
53	4, 52	anbi12d 473	. . 3 ⊢ (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+_g‘𝑟) / 𝑝][(._r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))) ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
54		df-ring 13181	. . 3 ⊢ Ring = {𝑟 ∈ Grp ∣ ((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+_g‘𝑟) / 𝑝][(._r‘𝑟) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
55	53, 54	elrab2 2897	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
56		3anass 982	. 2 ⊢ ((𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
57	55, 56	bitr4i 187	1 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))

Colors of variables: wff set class

Syntax hints: ∧ wa 104 ↔ wb 105 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ∀wral 2455 Vcvv 2738 [wsbc 2963 Fn wfn 5212 ‘cfv 5217 (class class class)co 5875 Basecbs 12462 +_gcplusg 12536 ._rcmulr 12537 Mndcmnd 12817 Grpcgrp 12877 mulGrpcmgp 13130 Ringcrg 13179

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4122 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-cnex 7902 ax-resscn 7903 ax-1re 7905 ax-addrcl 7908

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2740 df-sbc 2964 df-un 3134 df-in 3136 df-ss 3143 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-br 4005 df-opab 4066 df-mpt 4067 df-id 4294 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-iota 5179 df-fun 5219 df-fn 5220 df-fv 5225 df-ov 5878 df-inn 8920 df-2 8978 df-3 8979 df-ndx 12465 df-slot 12466 df-base 12468 df-plusg 12549 df-mulr 12550 df-ring 13181

This theorem is referenced by: ringgrp 13184 ringmgp 13185 ringdilem 13195 ringpropd 13217 isringd 13220 ringsrg 13224 ring1 13236

W3C validator