Metamath Proof Explorer


Theorem ldilco

Description: The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013)

Ref Expression
Hypotheses ldilco.h 𝐻 = ( LHyp ‘ 𝐾 )
ldilco.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
Assertion ldilco ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ( 𝐹𝐺 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 ldilco.h 𝐻 = ( LHyp ‘ 𝐾 )
2 ldilco.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
3 simp1l ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → 𝐾𝑉 )
4 eqid ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
5 1 4 2 ldillaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
6 5 3adant3 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
7 1 4 2 ldillaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐺𝐷 ) → 𝐺 ∈ ( LAut ‘ 𝐾 ) )
8 7 3adant2 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → 𝐺 ∈ ( LAut ‘ 𝐾 ) )
9 4 lautco ( ( 𝐾𝑉𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ 𝐺 ∈ ( LAut ‘ 𝐾 ) ) → ( 𝐹𝐺 ) ∈ ( LAut ‘ 𝐾 ) )
10 3 6 8 9 syl3anc ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ( 𝐹𝐺 ) ∈ ( LAut ‘ 𝐾 ) )
11 simp11 ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾𝑉𝑊𝐻 ) )
12 simp13 ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝐺𝐷 )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 1 2 ldil1o ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐺𝐷 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
15 11 12 14 syl2anc ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
16 f1of ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
17 15 16 syl ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
18 simp2 ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
19 fvco3 ( ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑥 ) ) )
20 17 18 19 syl2anc ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑥 ) ) )
21 simp3 ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝑥 ( le ‘ 𝐾 ) 𝑊 )
22 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
23 13 22 1 2 ldilval ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐺𝐷 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐺𝑥 ) = 𝑥 )
24 11 12 18 21 23 syl112anc ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐺𝑥 ) = 𝑥 )
25 24 fveq2d ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹 ‘ ( 𝐺𝑥 ) ) = ( 𝐹𝑥 ) )
26 simp12 ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → 𝐹𝐷 )
27 13 22 1 2 ldilval ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹𝑥 ) = 𝑥 )
28 11 26 18 21 27 syl112anc ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹𝑥 ) = 𝑥 )
29 20 25 28 3eqtrd ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = 𝑥 )
30 29 3exp ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = 𝑥 ) ) )
31 30 ralrimiv ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = 𝑥 ) )
32 13 22 1 4 2 isldil ( ( 𝐾𝑉𝑊𝐻 ) → ( ( 𝐹𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹𝐺 ) ∈ ( LAut ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = 𝑥 ) ) ) )
33 32 3ad2ant1 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ( ( 𝐹𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹𝐺 ) ∈ ( LAut ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝐹𝐺 ) ‘ 𝑥 ) = 𝑥 ) ) ) )
34 10 31 33 mpbir2and ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷𝐺𝐷 ) → ( 𝐹𝐺 ) ∈ 𝐷 )