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 ( 𝜑 → ( 𝐽𝑇 ↔ ( 𝐽𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝐽 ) ) ) ∈ 𝑌 ) ) )