Metamath Proof Explorer

Theorem mapdordlem1a

Description: Lemma for mapdord . (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdordlem1a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdordlem1a.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdordlem1a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdordlem1a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdordlem1a.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
mapdordlem1a.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdordlem1a.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdordlem1a.t ⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 }
mapdordlem1a.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
mapdordlem1a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion mapdordlem1a ( 𝜑 → ( 𝐽 ∈ 𝑇 ↔ ( 𝐽 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mapdordlem1a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdordlem1a.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdordlem1a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdordlem1a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 mapdordlem1a.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 mapdordlem1a.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 mapdordlem1a.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 mapdordlem1a.t ⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 }
9 mapdordlem1a.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
10 mapdordlem1a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 )
12 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → 𝐽 ∈ 𝐹 )
14 1 2 3 6 5 7 12 13 dochlkr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝐿 ‘ 𝐽 ) ∈ 𝑌 ) ) )
15 11 14 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝐿 ‘ 𝐽 ) ∈ 𝑌 ) )
16 15 simpld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) )
17 16 ex ⊢ ( 𝜑 → ( ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) )
18 17 pm4.71rd ⊢ ( 𝜑 → ( ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) ) )
19 2fveq3 ⊢ ( 𝑔 = 𝐽 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) )
20 19 fveq2d ⊢ ( 𝑔 = 𝐽 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) )
21 20 eleq1d ⊢ ( 𝑔 = 𝐽 → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝑌 ↔ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )
22 21 8 elrab2 ⊢ ( 𝐽 ∈ 𝑇 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )
23 9 lcfl1lem ⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) )
24 23 anbi1i ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) )
25 anass ⊢ ( ( ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ) ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ↔ ( 𝐽 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) )
26 an12 ⊢ ( ( 𝐽 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) )
27 24 25 26 3bitri ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ 𝐽 ) ∧ ( 𝐽 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) )
28 18 22 27 3bitr4g ⊢ ( 𝜑 → ( 𝐽 ∈ 𝑇 ↔ ( 𝐽 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝐽 ) ) ) ∈ 𝑌 ) ) )