Metamath Proof Explorer


Theorem dihglblem3N

Description: Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b 𝐵 = ( Base ‘ 𝐾 )
dihglblem.l = ( le ‘ 𝐾 )
dihglblem.m = ( meet ‘ 𝐾 )
dihglblem.g 𝐺 = ( glb ‘ 𝐾 )
dihglblem.h 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem.t 𝑇 = { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) }
dihglblem.i 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihglblem.ih 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihglblem3N ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐼 ‘ ( 𝐺𝑇 ) ) = 𝑥𝑇 ( 𝐼𝑥 ) )

Proof

Step Hyp Ref Expression
1 dihglblem.b 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem.l = ( le ‘ 𝐾 )
3 dihglblem.m = ( meet ‘ 𝐾 )
4 dihglblem.g 𝐺 = ( glb ‘ 𝐾 )
5 dihglblem.h 𝐻 = ( LHyp ‘ 𝐾 )
6 dihglblem.t 𝑇 = { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) }
7 dihglblem.i 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 dihglblem.ih 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝐾 ∈ HL )
11 10 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝐾 ∈ Lat )
12 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝑆𝐵 )
13 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝑣𝑆 )
14 12 13 sseldd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝑣𝐵 )
15 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝑊𝐻 )
16 1 5 lhpbase ( 𝑊𝐻𝑊𝐵 )
17 15 16 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → 𝑊𝐵 )
18 1 2 3 latmle2 ( ( 𝐾 ∈ Lat ∧ 𝑣𝐵𝑊𝐵 ) → ( 𝑣 𝑊 ) 𝑊 )
19 11 14 17 18 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵𝑣𝑆 ) → ( 𝑣 𝑊 ) 𝑊 )
20 19 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵 ) → ( 𝑣𝑆 → ( 𝑣 𝑊 ) 𝑊 ) )
21 breq1 ( 𝑢 = ( 𝑣 𝑊 ) → ( 𝑢 𝑊 ↔ ( 𝑣 𝑊 ) 𝑊 ) )
22 21 biimprcd ( ( 𝑣 𝑊 ) 𝑊 → ( 𝑢 = ( 𝑣 𝑊 ) → 𝑢 𝑊 ) )
23 20 22 syl6 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵 ) → ( 𝑣𝑆 → ( 𝑢 = ( 𝑣 𝑊 ) → 𝑢 𝑊 ) ) )
24 23 rexlimdv ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑢𝐵 ) → ( ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) → 𝑢 𝑊 ) )
25 24 ss2rabdv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) } ⊆ { 𝑢𝐵𝑢 𝑊 } )
26 6 25 eqsstrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑇 ⊆ { 𝑢𝐵𝑢 𝑊 } )
27 1 2 5 7 dibdmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → dom 𝐽 = { 𝑢𝐵𝑢 𝑊 } )
28 27 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → dom 𝐽 = { 𝑢𝐵𝑢 𝑊 } )
29 26 28 sseqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑇 ⊆ dom 𝐽 )
30 1 2 3 4 5 6 dihglblem2aN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ )
31 30 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑇 ≠ ∅ )
32 4 5 7 dibglbN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑇 ⊆ dom 𝐽𝑇 ≠ ∅ ) ) → ( 𝐽 ‘ ( 𝐺𝑇 ) ) = 𝑥𝑇 ( 𝐽𝑥 ) )
33 9 29 31 32 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐽 ‘ ( 𝐺𝑇 ) ) = 𝑥𝑇 ( 𝐽𝑥 ) )
34 1 2 3 4 5 6 dihglblem2N ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) = ( 𝐺𝑇 ) )
35 34 3adant2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) = ( 𝐺𝑇 ) )
36 35 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐽 ‘ ( 𝐺𝑆 ) ) = ( 𝐽 ‘ ( 𝐺𝑇 ) ) )
37 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
38 26 sselda ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑇 ) → 𝑥 ∈ { 𝑢𝐵𝑢 𝑊 } )
39 breq1 ( 𝑢 = 𝑥 → ( 𝑢 𝑊𝑥 𝑊 ) )
40 39 elrab ( 𝑥 ∈ { 𝑢𝐵𝑢 𝑊 } ↔ ( 𝑥𝐵𝑥 𝑊 ) )
41 38 40 sylib ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑇 ) → ( 𝑥𝐵𝑥 𝑊 ) )
42 1 2 5 8 7 dihvalb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝐵𝑥 𝑊 ) ) → ( 𝐼𝑥 ) = ( 𝐽𝑥 ) )
43 37 41 42 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑇 ) → ( 𝐼𝑥 ) = ( 𝐽𝑥 ) )
44 43 iineq2dv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑥𝑇 ( 𝐼𝑥 ) = 𝑥𝑇 ( 𝐽𝑥 ) )
45 33 36 44 3eqtr4rd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑥𝑇 ( 𝐼𝑥 ) = ( 𝐽 ‘ ( 𝐺𝑆 ) ) )
46 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝐾 ∈ HL )
47 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
48 46 47 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝐾 ∈ CLat )
49 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑆𝐵 )
50 1 4 clatglbcl ( ( 𝐾 ∈ CLat ∧ 𝑆𝐵 ) → ( 𝐺𝑆 ) ∈ 𝐵 )
51 48 49 50 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) ∈ 𝐵 )
52 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) 𝑊 )
53 1 2 5 8 7 dihvalb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐺𝑆 ) ∈ 𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝐺𝑆 ) ) = ( 𝐽 ‘ ( 𝐺𝑆 ) ) )
54 9 51 52 53 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐼 ‘ ( 𝐺𝑆 ) ) = ( 𝐽 ‘ ( 𝐺𝑆 ) ) )
55 35 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐼 ‘ ( 𝐺𝑆 ) ) = ( 𝐼 ‘ ( 𝐺𝑇 ) ) )
56 45 54 55 3eqtr2rd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐵𝑆 ≠ ∅ ) ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐼 ‘ ( 𝐺𝑇 ) ) = 𝑥𝑇 ( 𝐼𝑥 ) )