rngomndo

Description: In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	unmnd.1	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	Assertion	rngomndo	⊢ ( 𝑅 ∈ RingOps → 𝐻 ∈ MndOp )

Proof

Step	Hyp	Ref	Expression
1		unmnd.1	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
2		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
3		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
4	2 1 3	rngosm	⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) )
5	2 1 3	rngoass	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
6	5	ralrimivvva	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
7	2 1 3	rngoi	⊢ ( 𝑅 ∈ RingOps → ( ( ( 1^st ‘ 𝑅 ) ∈ AbelOp ∧ 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ) ∧ ( ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 ( 1^st ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) ( 1^st ‘ 𝑅 ) ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) ( 1^st ‘ 𝑅 ) ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
8	7	simprrd	⊢ ( 𝑅 ∈ RingOps → ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
9	1 2	rngorn1	⊢ ( 𝑅 ∈ RingOps → ran ( 1^st ‘ 𝑅 ) = dom dom 𝐻 )
10		xpid11	⊢ ( ( dom dom 𝐻 × dom dom 𝐻 ) = ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ↔ dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) )
11	10	biimpri	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( dom dom 𝐻 × dom dom 𝐻 ) = ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) )
12		feq23	⊢ ( ( ( dom dom 𝐻 × dom dom 𝐻 ) = ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ∧ dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) ) → ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ↔ 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ) )
13	11 12	mpancom	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ↔ 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ) )
14		raleq	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ↔ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ) )
15	14	raleqbi1dv	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ↔ ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ) )
16	15	raleqbi1dv	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ↔ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ) )
17		raleq	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
18	17	rexeqbi1dv	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
19	13 16 18	3anbi123d	⊢ ( dom dom 𝐻 = ran ( 1^st ‘ 𝑅 ) → ( ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ↔ ( 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
20	19	eqcoms	⊢ ( ran ( 1^st ‘ 𝑅 ) = dom dom 𝐻 → ( ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ↔ ( 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
21	9 20	syl	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ↔ ( 𝐻 : ( ran ( 1^st ‘ 𝑅 ) × ran ( 1^st ‘ 𝑅 ) ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
22	4 6 8 21	mpbir3and	⊢ ( 𝑅 ∈ RingOps → ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
23		fvex	⊢ ( 2^nd ‘ 𝑅 ) ∈ V
24		eleq1	⊢ ( 𝐻 = ( 2^nd ‘ 𝑅 ) → ( 𝐻 ∈ V ↔ ( 2^nd ‘ 𝑅 ) ∈ V ) )
25	23 24	mpbiri	⊢ ( 𝐻 = ( 2^nd ‘ 𝑅 ) → 𝐻 ∈ V )
26		eqid	⊢ dom dom 𝐻 = dom dom 𝐻
27	26	ismndo1	⊢ ( 𝐻 ∈ V → ( 𝐻 ∈ MndOp ↔ ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
28	1 25 27	mp2b	⊢ ( 𝐻 ∈ MndOp ↔ ( 𝐻 : ( dom dom 𝐻 × dom dom 𝐻 ) ⟶ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ∀ 𝑧 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐻 ∀ 𝑦 ∈ dom dom 𝐻 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
29	22 28	sylibr	⊢ ( 𝑅 ∈ RingOps → 𝐻 ∈ MndOp )

Metamath Proof Explorer

Theorem rngomndo

Proof