Metamath Proof Explorer

Theorem dochkrshp4

Description: Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochkrshp3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochkrshp3.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkrshp3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochkrshp3.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochkrshp3.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochkrshp3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochkrshp3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion dochkrshp4 ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 dochkrshp3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkrshp3.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkrshp3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkrshp3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochkrshp3.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 dochkrshp3.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 dochkrshp3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dochkrshp3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 df-ne ⊢ ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 )
10 1 2 3 4 5 6 7 8 dochkrshp3 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) )
11 10 biimprd ⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
12 11 expdimp ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
13 9 12 syl5bir ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
14 13 orrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
15 14 orcomd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
16 15 ex ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
17 simpl ⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
18 10 17 syl6bi ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
19 1 3 2 4 7 dochoc1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
20 2fveq3 ⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
21 id ⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
22 20 21 eqeq12d ⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 ) )
23 19 22 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
24 18 23 jaod ⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
25 16 24 impbid ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )