Metamath Proof Explorer

Theorem dihglb2

Description: Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dihglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglb.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihglb2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihglb2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
Assertion dihglb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐼 ‘ ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ∩ { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } )

Proof

Step Hyp Ref Expression
1 dihglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 dihglb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihglb.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dihglb2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 dihglb2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
7 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ⊆ 𝐵
9 8 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ⊆ 𝐵 )
10 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
11 10 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → 𝐾 ∈ OP )
12 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
13 1 12 op1cl ⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ 𝐵 )
14 11 13 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 1. ‘ 𝐾 ) ∈ 𝐵 )
15 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
16 12 3 4 5 6 dih1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) = 𝑉 )
17 16 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) = 𝑉 )
18 15 17 sseqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) )
19 fveq2 ⊢ ( 𝑥 = ( 1. ‘ 𝐾 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) )
20 19 sseq2d ⊢ ( 𝑥 = ( 1. ‘ 𝐾 ) → ( 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) ↔ 𝑆 ⊆ ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) ) )
21 20 elrab ⊢ ( ( 1. ‘ 𝐾 ) ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ↔ ( ( 1. ‘ 𝐾 ) ∈ 𝐵 ∧ 𝑆 ⊆ ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) ) )
22 14 18 21 sylanbrc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 1. ‘ 𝐾 ) ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } )
23 22 ne0d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ≠ ∅ )
24 1 2 3 4 dihglb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ⊆ 𝐵 ∧ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ∩ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ( 𝐼 ‘ 𝑧 ) )
25 7 9 23 24 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐼 ‘ ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ∩ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ( 𝐼 ‘ 𝑧 ) )
26 fvex ⊢ ( 𝐼 ‘ 𝑧 ) ∈ V
27 26 dfiin2 ⊢ ∩ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ( 𝐼 ‘ 𝑧 ) = ∩ { 𝑦 ∣ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) }
28 1 3 4 dihfn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn 𝐵 )
29 28 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑆 ⊆ 𝑦 ) → 𝐼 Fn 𝐵 )
30 fvelrnb ⊢ ( 𝐼 Fn 𝐵 → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝐼 ‘ 𝑧 ) = 𝑦 ) )
31 29 30 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑆 ⊆ 𝑦 ) → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝐼 ‘ 𝑧 ) = 𝑦 ) )
32 eqcom ⊢ ( ( 𝐼 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝐼 ‘ 𝑧 ) )
33 32 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝐼 ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 = ( 𝐼 ‘ 𝑧 ) )
34 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐵 𝑦 = ( 𝐼 ‘ 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) )
35 33 34 bitri ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝐼 ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) )
36 31 35 bitrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑆 ⊆ 𝑦 ) → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ) )
37 36 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 ⊆ 𝑦 → ( 𝑦 ∈ ran 𝐼 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ) ) )
38 37 pm5.32rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( ( 𝑦 ∈ ran 𝐼 ∧ 𝑆 ⊆ 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) ) )
39 df-rex ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) )
40 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑧 ) )
41 40 sseq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) ↔ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
42 41 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
43 42 anbi1i ⊢ ( ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) )
44 sseq2 ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑧 ) → ( 𝑆 ⊆ 𝑦 ↔ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) )
45 44 anbi2d ⊢ ( 𝑦 = ( 𝐼 ‘ 𝑧 ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) ) )
46 45 pm5.32ri ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ 𝑦 ) ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) )
47 an32 ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ 𝑦 ) ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) )
48 43 46 47 3bitr2i ⊢ ( ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) )
49 48 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) )
50 19.41v ⊢ ( ∃ 𝑧 ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) )
51 39 49 50 3bitrri ⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ 𝑦 = ( 𝐼 ‘ 𝑧 ) ) ∧ 𝑆 ⊆ 𝑦 ) ↔ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) )
52 38 51 bitr2di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) ↔ ( 𝑦 ∈ ran 𝐼 ∧ 𝑆 ⊆ 𝑦 ) ) )
53 52 abbidv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → { 𝑦 ∣ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) } = { 𝑦 ∣ ( 𝑦 ∈ ran 𝐼 ∧ 𝑆 ⊆ 𝑦 ) } )
54 df-rab ⊢ { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ ran 𝐼 ∧ 𝑆 ⊆ 𝑦 ) }
55 53 54 eqtr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → { 𝑦 ∣ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) } = { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } )
56 55 inteqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑦 ∣ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } 𝑦 = ( 𝐼 ‘ 𝑧 ) } = ∩ { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } )
57 27 56 syl5eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ∩ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ( 𝐼 ‘ 𝑧 ) = ∩ { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } )
58 25 57 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐼 ‘ ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ∩ { 𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦 } )