Metamath Proof Explorer

Theorem lclkrlem2y

Description: Lemma for lclkr . Restate the hypotheses for E and G to say their kernels are closed, in order to eliminate the generating vectors X and Y . (Contributed by NM, 18-Jan-2015)

Ref Expression
Hypotheses lclkrlem2y.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2y.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2y.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2y.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2y.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2y.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2y.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2y.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2y.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2y.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2y.le ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) )
lclkrlem2y.lg ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
Assertion lclkrlem2y ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2y.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
2 lclkrlem2y.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 lclkrlem2y.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2y.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 lclkrlem2y.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 lclkrlem2y.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
7 lclkrlem2y.p ⊢ + = ( +g ‘ 𝐷 )
8 lclkrlem2y.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 lclkrlem2y.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
10 lclkrlem2y.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11 lclkrlem2y.le ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) )
12 lclkrlem2y.lg ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
13 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
14 2 3 4 13 5 1 8 10 lcfl8a ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) )
15 12 14 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) )
16 2 3 4 13 5 1 8 9 lcfl8a ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ) )
17 11 16 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) )
18 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → 𝑥 ∈ ( Base ‘ 𝑈 ) )
20 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → 𝑦 ∈ ( Base ‘ 𝑈 ) )
21 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → 𝐸 ∈ 𝐹 )
22 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → 𝐺 ∈ 𝐹 )
23 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) )
24 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) )
25 1 2 3 4 13 5 6 7 18 19 20 21 22 23 24 lclkrlem2x ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
26 25 3exp ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) )
27 26 3expd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑈 ) → ( ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) → ( 𝑦 ∈ ( Base ‘ 𝑈 ) → ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) ) ) )
28 27 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑥 } ) → ( 𝑦 ∈ ( Base ‘ 𝑈 ) → ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) ) )
29 17 28 mpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝑈 ) → ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) )
30 29 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑦 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
31 15 30 mpd ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )