Metamath Proof Explorer


Theorem lkrss2N

Description: Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrss2.s S = Scalar W
lkrss2.r R = Base S
lkrss2.f F = LFnl W
lkrss2.k K = LKer W
lkrss2.d D = LDual W
lkrss2.t · ˙ = D
lkrss2.w φ W LVec
lkrss2.g φ G F
lkrss2.h φ H F
Assertion lkrss2N φ K G K H r R H = r · ˙ G

Proof

Step Hyp Ref Expression
1 lkrss2.s S = Scalar W
2 lkrss2.r R = Base S
3 lkrss2.f F = LFnl W
4 lkrss2.k K = LKer W
5 lkrss2.d D = LDual W
6 lkrss2.t · ˙ = D
7 lkrss2.w φ W LVec
8 lkrss2.g φ G F
9 lkrss2.h φ H F
10 sspss K G K H K G K H K G = K H
11 eqid 0 D = 0 D
12 3 4 5 11 7 8 9 lkrpssN φ K G K H G 0 D H = 0 D
13 lveclmod W LVec W LMod
14 7 13 syl φ W LMod
15 eqid 0 S = 0 S
16 1 2 15 lmod0cl W LMod 0 S R
17 14 16 syl φ 0 S R
18 17 adantr φ H = 0 D 0 S R
19 simpr φ H = 0 D H = 0 D
20 3 1 15 5 6 11 14 8 ldual0vs φ 0 S · ˙ G = 0 D
21 20 adantr φ H = 0 D 0 S · ˙ G = 0 D
22 19 21 eqtr4d φ H = 0 D H = 0 S · ˙ G
23 oveq1 r = 0 S r · ˙ G = 0 S · ˙ G
24 23 rspceeqv 0 S R H = 0 S · ˙ G r R H = r · ˙ G
25 18 22 24 syl2anc φ H = 0 D r R H = r · ˙ G
26 25 ex φ H = 0 D r R H = r · ˙ G
27 26 adantld φ G 0 D H = 0 D r R H = r · ˙ G
28 12 27 sylbid φ K G K H r R H = r · ˙ G
29 28 imp φ K G K H r R H = r · ˙ G
30 7 adantr φ K G = K H W LVec
31 8 adantr φ K G = K H G F
32 9 adantr φ K G = K H H F
33 simpr φ K G = K H K G = K H
34 1 2 3 4 5 6 30 31 32 33 eqlkr4 φ K G = K H r R H = r · ˙ G
35 29 34 jaodan φ K G K H K G = K H r R H = r · ˙ G
36 10 35 sylan2b φ K G K H r R H = r · ˙ G
37 7 adantr φ r R W LVec
38 8 adantr φ r R G F
39 simpr φ r R r R
40 1 2 3 4 5 6 37 38 39 lkrss φ r R K G K r · ˙ G
41 40 ex φ r R K G K r · ˙ G
42 fveq2 H = r · ˙ G K H = K r · ˙ G
43 42 sseq2d H = r · ˙ G K G K H K G K r · ˙ G
44 43 biimprcd K G K r · ˙ G H = r · ˙ G K G K H
45 41 44 syl6 φ r R H = r · ˙ G K G K H
46 45 rexlimdv φ r R H = r · ˙ G K G K H
47 46 imp φ r R H = r · ˙ G K G K H
48 36 47 impbida φ K G K H r R H = r · ˙ G