df-dlat

Description: Adistributive lattice is a lattice in which meets distribute over joins, or equivalently ( latdisd ) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Assertion	df-dlat	⊢ DLat = { 𝑘 ∈ Lat ∣ [ ( Base ‘ 𝑘 ) / 𝑏 ] [ ( join ‘ 𝑘 ) / 𝑗 ] [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdlat	⊢ DLat
1		vk	⊢ 𝑘
2		clat	⊢ Lat
3		cbs	⊢ Base
4	1	cv	⊢ 𝑘
5	4 3	cfv	⊢ ( Base ‘ 𝑘 )
6		vb	⊢ 𝑏
7		cjn	⊢ join
8	4 7	cfv	⊢ ( join ‘ 𝑘 )
9		vj	⊢ 𝑗
10		cmee	⊢ meet
11	4 10	cfv	⊢ ( meet ‘ 𝑘 )
12		vm	⊢ 𝑚
13		vx	⊢ 𝑥
14	6	cv	⊢ 𝑏
15		vy	⊢ 𝑦
16		vz	⊢ 𝑧
17	13	cv	⊢ 𝑥
18	12	cv	⊢ 𝑚
19	15	cv	⊢ 𝑦
20	9	cv	⊢ 𝑗
21	16	cv	⊢ 𝑧
22	19 21 20	co	⊢ ( 𝑦 𝑗 𝑧 )
23	17 22 18	co	⊢ ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) )
24	17 19 18	co	⊢ ( 𝑥 𝑚 𝑦 )
25	17 21 18	co	⊢ ( 𝑥 𝑚 𝑧 )
26	24 25 20	co	⊢ ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
27	23 26	wceq	⊢ ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
28	27 16 14	wral	⊢ ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
29	28 15 14	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
30	29 13 14	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
31	30 12 11	wsbc	⊢ [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
32	31 9 8	wsbc	⊢ [ ( join ‘ 𝑘 ) / 𝑗 ] [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
33	32 6 5	wsbc	⊢ [ ( Base ‘ 𝑘 ) / 𝑏 ] [ ( join ‘ 𝑘 ) / 𝑗 ] [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) )
34	33 1 2	crab	⊢ { 𝑘 ∈ Lat ∣ [ ( Base ‘ 𝑘 ) / 𝑏 ] [ ( join ‘ 𝑘 ) / 𝑗 ] [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) ) }
35	0 34	wceq	⊢ DLat = { 𝑘 ∈ Lat ∣ [ ( Base ‘ 𝑘 ) / 𝑏 ] [ ( join ‘ 𝑘 ) / 𝑗 ] [ ( meet ‘ 𝑘 ) / 𝑚 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑚 ( 𝑦 𝑗 𝑧 ) ) = ( ( 𝑥 𝑚 𝑦 ) 𝑗 ( 𝑥 𝑚 𝑧 ) ) }

Metamath Proof Explorer

Definition df-dlat

Detailed syntax breakdown