irredmul

Description: If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irredmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irredmul.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	irredmul.t	⊢ · = ( ._r ‘ 𝑅 )
Assertion	irredmul	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐼 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irredmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		irredmul.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
4		irredmul.t	⊢ · = ( ._r ‘ 𝑅 )
5	2 3 1 4	isirred2	⊢ ( ( 𝑋 · 𝑌 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ¬ ( 𝑋 · 𝑌 ) ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
6	5	simp3bi	⊢ ( ( 𝑋 · 𝑌 ) ∈ 𝐼 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
7		eqid	⊢ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 )
8		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑦 ) )
9	8	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ↔ ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) )
10		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
11	10	orbi1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ↔ ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
12	9 11	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
13		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
14	13	eqeq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) ↔ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) ) )
15		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )
16	15	orbi2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ↔ ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
17	14 16	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) ) )
18	12 17	rspc2v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) ) )
19	7 18	mpii	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
20	6 19	syl5	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝐼 → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
21	20	3impia	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐼 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) )

Metamath Proof Explorer

Theorem irredmul

Proof