Theorem latm4

Description: Rearrangement of lattice meet of 4 classes. ( in4 analog.) (Contributed by NM, 8-Nov-2011)

	Ref	Expression
Hypotheses	olmass.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	olmass.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latm4	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑍 ∧ 𝑊 ) ) = ( ( 𝑋 ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		olmass.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		olmass.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		simp1	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐾 ∈ OL )
4		simp2r	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
5		simp3l	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
6		simp3r	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
7	1 2	latm12	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑌 ∧ ( 𝑍 ∧ 𝑊 ) ) = ( 𝑍 ∧ ( 𝑌 ∧ 𝑊 ) ) )
8	3 4 5 6 7	syl13anc	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑌 ∧ ( 𝑍 ∧ 𝑊 ) ) = ( 𝑍 ∧ ( 𝑌 ∧ 𝑊 ) ) )
9	8	oveq2d	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑋 ∧ ( 𝑌 ∧ ( 𝑍 ∧ 𝑊 ) ) ) = ( 𝑋 ∧ ( 𝑍 ∧ ( 𝑌 ∧ 𝑊 ) ) ) )
10		simp2l	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11		ollat	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat )
12	11	3ad2ant1	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
13	1 2	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 ∧ 𝑊 ) ∈ 𝐵 )
14	12 5 6 13	syl3anc	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑍 ∧ 𝑊 ) ∈ 𝐵 )
15	1 2	latmassOLD	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑍 ∧ 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑍 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑌 ∧ ( 𝑍 ∧ 𝑊 ) ) ) )
16	3 10 4 14 15	syl13anc	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑍 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑌 ∧ ( 𝑍 ∧ 𝑊 ) ) ) )
17	1 2	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
18	12 4 6 17	syl3anc	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
19	1 2	latmassOLD	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑍 ∧ ( 𝑌 ∧ 𝑊 ) ) ) )
20	3 10 5 18 19	syl13anc	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑍 ∧ ( 𝑌 ∧ 𝑊 ) ) ) )
21	9 16 20	3eqtr4d	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑍 ∧ 𝑊 ) ) = ( ( 𝑋 ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑊 ) ) )