Metamath Proof Explorer


Theorem dih1dimb2

Description: Isomorphism H at an atom under W . (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dih1dimb2.b 𝐵 = ( Base ‘ 𝐾 )
dih1dimb2.l = ( le ‘ 𝐾 )
dih1dimb2.a 𝐴 = ( Atoms ‘ 𝐾 )
dih1dimb2.h 𝐻 = ( LHyp ‘ 𝐾 )
dih1dimb2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dih1dimb2.o 𝑂 = ( 𝑇 ↦ ( I ↾ 𝐵 ) )
dih1dimb2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimb2.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimb2.n 𝑁 = ( LSpan ‘ 𝑈 )
Assertion dih1dimb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) → ∃ 𝑓𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 dih1dimb2.b 𝐵 = ( Base ‘ 𝐾 )
2 dih1dimb2.l = ( le ‘ 𝐾 )
3 dih1dimb2.a 𝐴 = ( Atoms ‘ 𝐾 )
4 dih1dimb2.h 𝐻 = ( LHyp ‘ 𝐾 )
5 dih1dimb2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 dih1dimb2.o 𝑂 = ( 𝑇 ↦ ( I ↾ 𝐵 ) )
7 dih1dimb2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dih1dimb2.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 dih1dimb2.n 𝑁 = ( LSpan ‘ 𝑈 )
10 eqid ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11 2 3 4 5 10 cdlemf ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) → ∃ 𝑓𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 )
12 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 )
13 simp1rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑄𝐴 )
14 12 13 eqeltrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 )
15 simp1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
16 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓𝑇 )
17 1 3 4 5 10 trlnidatb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓𝑇 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) )
18 15 16 17 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) )
19 14 18 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓 ≠ ( I ↾ 𝐵 ) )
20 12 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝐼𝑄 ) )
21 1 4 5 10 6 7 8 9 dih1dimb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓𝑇 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
22 15 16 21 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
23 20 22 eqtr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
24 19 23 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )
25 24 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) ∧ 𝑓𝑇 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) ) )
26 25 reximdva ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) → ( ∃ 𝑓𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ∃ 𝑓𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) ) )
27 11 26 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴𝑄 𝑊 ) ) → ∃ 𝑓𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )