This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lautm

Description: Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012)

Ref Expression
Hypotheses lautm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lautm.m ⊢ ∧ = ( meet ‘ 𝐾 )
lautm.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautm ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lautm.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 lautm.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
6 simpr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐼 )
7 5 6 jca ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) )
8 1 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
9 8 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
10 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ 𝐵 )
11 7 9 10 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ 𝐵 )
12 simpr2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
13 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
14 7 12 13 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
15 simpr3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
16 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
17 7 15 16 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
18 1 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 )
19 5 14 17 18 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 )
20 1 4 2 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
21 20 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
22 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
23 7 9 12 22 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
24 21 23 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) )
25 1 4 2 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
26 25 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
27 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
28 7 9 15 27 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
29 26 28 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) )
30 1 4 2 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) )
31 5 11 14 17 30 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) )
32 24 29 31 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) )
33 1 3 laut1o ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
34 33 3ad2antr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
35 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) )
36 34 19 35 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) )
37 1 4 2 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) )
38 5 14 17 37 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) )
39 1 4 3 lautcnvle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
40 7 19 14 39 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
41 38 40 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) )
42 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
43 34 12 42 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
44 41 43 breqtrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 )
45 1 4 2 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) )
46 5 14 17 45 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) )
47 1 4 3 lautcnvle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )
48 7 19 17 47 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )
49 46 48 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑌 ) ) )
50 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
51 34 15 50 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
52 49 51 breqtrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 )
53 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 )
54 34 19 53 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 )
55 1 4 2 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) )
56 5 54 12 15 55 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) )
57 44 52 56 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) )
58 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
59 7 54 9 58 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
60 57 59 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) )
61 36 60 eqbrtrrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) )
62 1 4 5 11 19 32 61 latasymd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑌 ) ) )