df-mpq

Description: Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.4 of Gleason p. 119. (Contributed by NM, 28-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-mpq	⊢ ·_pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpq	⊢ ·_pQ
1		vx	⊢ 𝑥
2		cnpi	⊢ N
3	2 2	cxp	⊢ ( N × N )
4		vy	⊢ 𝑦
5		c1st	⊢ 1^st
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( 1^st ‘ 𝑥 )
8		cmi	⊢ ·_N
9	4	cv	⊢ 𝑦
10	9 5	cfv	⊢ ( 1^st ‘ 𝑦 )
11	7 10 8	co	⊢ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) )
12		c2nd	⊢ 2^nd
13	6 12	cfv	⊢ ( 2^nd ‘ 𝑥 )
14	9 12	cfv	⊢ ( 2^nd ‘ 𝑦 )
15	13 14 8	co	⊢ ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) )
16	11 15	cop	⊢ ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩
17	1 4 3 3 16	cmpo	⊢ ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )
18	0 17	wceq	⊢ ·_pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )

Metamath Proof Explorer

Definition df-mpq

Detailed syntax breakdown