Theorem dvdsrpropd

Description: The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

	Ref	Expression
Hypotheses	rngidpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	rngidpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	rngidpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion	dvdsrpropd	⊢ ( 𝜑 → ( ∥r ‘ 𝐾 ) = ( ∥r ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		rngidpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		rngidpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		rngidpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
4	3	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5	4	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ↔ ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) )
6	5	an32s	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ↔ ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) )
7	6	rexbidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) )
8	7	pm5.32da	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) ) )
9	1	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
10	1	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) )
11	9 10	anbi12d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) ) )
12	2	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐿 ) ) )
13	2	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) )
14	12 13	anbi12d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐿 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) ) )
15	8 11 14	3bitr3d	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐿 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) ) )
16	15	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( Base ‘ 𝐿 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) } )
17		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18		eqid	⊢ ( ∥r ‘ 𝐾 ) = ( ∥r ‘ 𝐾 )
19		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
20	17 18 19	dvdsrval	⊢ ( ∥r ‘ 𝐾 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = 𝑧 ) }
21		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
22		eqid	⊢ ( ∥r ‘ 𝐿 ) = ( ∥r ‘ 𝐿 )
23		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
24	21 22 23	dvdsrval	⊢ ( ∥r ‘ 𝐿 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( Base ‘ 𝐿 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = 𝑧 ) }
25	16 20 24	3eqtr4g	⊢ ( 𝜑 → ( ∥r ‘ 𝐾 ) = ( ∥r ‘ 𝐿 ) )