This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihmeetlem4N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem4.l ⊢ ≤ = ( le ‘ 𝐾 )
dihmeetlem4.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeetlem4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihmeetlem4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.z ⊢ 0 = ( 0g ‘ 𝑈 )
Assertion dihmeetlem4N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dihmeetlem4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihmeetlem4.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dihmeetlem4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dihmeetlem4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dihmeetlem4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 dihmeetlem4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dihmeetlem4.z ⊢ 0 = ( 0g ‘ 𝑈 )
9 eqid ⊢ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
10 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
12 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dihmeetlem4preN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = { 0 } )