iscrngo2

Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010)

	Ref	Expression
Hypotheses	iscring2.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	iscring2.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	iscring2.3	⊢ 𝑋 = ran 𝐺
Assertion	iscrngo2	⊢ ( 𝑅 ∈ CRingOps ↔ ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscring2.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		iscring2.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		iscring2.3	⊢ 𝑋 = ran 𝐺
4		iscrngo	⊢ ( 𝑅 ∈ CRingOps ↔ ( 𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2 ) )
5		relrngo	⊢ Rel RingOps
6		1st2nd	⊢ ( ( Rel RingOps ∧ 𝑅 ∈ RingOps ) → 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ )
7	5 6	mpan	⊢ ( 𝑅 ∈ RingOps → 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ )
8		eleq1	⊢ ( 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ → ( 𝑅 ∈ Com2 ↔ ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ ∈ Com2 ) )
9	1	rneqi	⊢ ran 𝐺 = ran ( 1^st ‘ 𝑅 )
10	3 9	eqtri	⊢ 𝑋 = ran ( 1^st ‘ 𝑅 )
11	10	raleqi	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) )
12	2	oveqi	⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 )
13	2	oveqi	⊢ ( 𝑦 𝐻 𝑥 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 )
14	12 13	eqeq12i	⊢ ( ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) )
15	10 14	raleqbii	⊢ ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) )
16	15	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) )
17		fvex	⊢ ( 1^st ‘ 𝑅 ) ∈ V
18		fvex	⊢ ( 2^nd ‘ 𝑅 ) ∈ V
19		iscom2	⊢ ( ( ( 1^st ‘ 𝑅 ) ∈ V ∧ ( 2^nd ‘ 𝑅 ) ∈ V ) → ( ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ ∈ Com2 ↔ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) ) )
20	17 18 19	mp2an	⊢ ( ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ ∈ Com2 ↔ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝑅 ) 𝑥 ) )
21	11 16 20	3bitr4ri	⊢ ( ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ ∈ Com2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
22	8 21	bitrdi	⊢ ( 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ → ( 𝑅 ∈ Com2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
23	7 22	syl	⊢ ( 𝑅 ∈ RingOps → ( 𝑅 ∈ Com2 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
24	23	pm5.32i	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2 ) ↔ ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
25	4 24	bitri	⊢ ( 𝑅 ∈ CRingOps ↔ ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )

Metamath Proof Explorer

Theorem iscrngo2

Proof