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 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝐷 )