Metamath Proof Explorer

Theorem dihglblem5aN

Description: A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem5a.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem5a.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihglblem5a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem5a.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihglblem5aN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 dihglblem5a.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem5a.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 dihglblem5a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihglblem5a.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ( le ‘ 𝐾 ) 𝑊 )
6 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝐾 ∈ Lat )
8 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 ∈ 𝐵 )
9 1 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
10 9 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑊 ∈ 𝐵 )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ∧ 𝑊 ) = 𝑋 ) )
13 7 8 10 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ∧ 𝑊 ) = 𝑋 ) )
14 5 13 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ∧ 𝑊 ) = 𝑋 )
15 14 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( 𝐼 ‘ 𝑋 ) )
16 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 1 11 3 4 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑊 ) ↔ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
18 16 8 10 17 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑊 ) ↔ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
19 5 18 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑊 ) )
20 df-ss ⊢ ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑊 ) ↔ ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) = ( 𝐼 ‘ 𝑋 ) )
21 19 20 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) = ( 𝐼 ‘ 𝑋 ) )
22 15 21 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
23 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
24 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
25 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
26 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
27 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
28 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
29 eqid ⊢ ( ℩ ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ℎ ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) = ( ℩ ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ℎ ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 )
30 eqid ⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) )
31 1 2 3 4 11 23 24 25 26 27 28 29 30 dihglblem5apreN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
32 31 anassrs ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )
33 22 32 pm2.61dan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑊 ) ) )