Metamath Proof Explorer


Theorem hdmapglem7

Description: Lemma for hdmapg . Line 15 in Baer p. 111, f(x,y) alpha = f(y,x). In the proof, our E , ( O{ E } ) , X , Y , k , u , l , and v correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ( ( SY )X ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapglem7.h H = LHyp K
hdmapglem7.e E = I Base K I LTrn K W
hdmapglem7.o O = ocH K W
hdmapglem7.u U = DVecH K W
hdmapglem7.v V = Base U
hdmapglem7.p + ˙ = + U
hdmapglem7.q · ˙ = U
hdmapglem7.r R = Scalar U
hdmapglem7.b B = Base R
hdmapglem7.a ˙ = LSSum U
hdmapglem7.n N = LSpan U
hdmapglem7.k φ K HL W H
hdmapglem7.x φ X V
hdmapglem7.t × ˙ = R
hdmapglem7.z 0 ˙ = 0 R
hdmapglem7.c ˙ = + R
hdmapglem7.s S = HDMap K W
hdmapglem7.g G = HGMap K W
hdmapglem7.y φ Y V
Assertion hdmapglem7 φ G S Y X = S X Y

Proof

Step Hyp Ref Expression
1 hdmapglem7.h H = LHyp K
2 hdmapglem7.e E = I Base K I LTrn K W
3 hdmapglem7.o O = ocH K W
4 hdmapglem7.u U = DVecH K W
5 hdmapglem7.v V = Base U
6 hdmapglem7.p + ˙ = + U
7 hdmapglem7.q · ˙ = U
8 hdmapglem7.r R = Scalar U
9 hdmapglem7.b B = Base R
10 hdmapglem7.a ˙ = LSSum U
11 hdmapglem7.n N = LSpan U
12 hdmapglem7.k φ K HL W H
13 hdmapglem7.x φ X V
14 hdmapglem7.t × ˙ = R
15 hdmapglem7.z 0 ˙ = 0 R
16 hdmapglem7.c ˙ = + R
17 hdmapglem7.s S = HDMap K W
18 hdmapglem7.g G = HGMap K W
19 hdmapglem7.y φ Y V
20 1 2 3 4 5 6 7 8 9 10 11 12 13 hdmapglem7a φ u O E k B X = k · ˙ E + ˙ u
21 1 2 3 4 5 6 7 8 9 10 11 12 19 hdmapglem7a φ v O E l B Y = l · ˙ E + ˙ v
22 12 ad2antrr φ u O E k B v O E l B K HL W H
23 1 4 12 dvhlmod φ U LMod
24 8 lmodring U LMod R Ring
25 23 24 syl φ R Ring
26 25 ad2antrr φ u O E k B v O E l B R Ring
27 simplrr φ u O E k B v O E l B k B
28 simprr φ u O E k B v O E l B l B
29 1 4 8 9 18 22 28 hgmapcl φ u O E k B v O E l B G l B
30 9 14 ringcl R Ring k B G l B k × ˙ G l B
31 26 27 29 30 syl3anc φ u O E k B v O E l B k × ˙ G l B
32 eqid Base K = Base K
33 eqid LTrn K W = LTrn K W
34 eqid 0 U = 0 U
35 1 32 33 4 5 34 2 12 dvheveccl φ E V 0 U
36 35 eldifad φ E V
37 36 snssd φ E V
38 1 4 5 3 dochssv K HL W H E V O E V
39 12 37 38 syl2anc φ O E V
40 39 ad2antrr φ u O E k B v O E l B O E V
41 simplrl φ u O E k B v O E l B u O E
42 40 41 sseldd φ u O E k B v O E l B u V
43 simprl φ u O E k B v O E l B v O E
44 40 43 sseldd φ u O E k B v O E l B v V
45 1 4 5 8 9 17 22 42 44 hdmapipcl φ u O E k B v O E l B S v u B
46 1 4 8 9 16 18 22 31 45 hgmapadd φ u O E k B v O E l B G k × ˙ G l ˙ S v u = G k × ˙ G l ˙ G S v u
47 1 4 8 9 14 18 22 27 29 hgmapmul φ u O E k B v O E l B G k × ˙ G l = G G l × ˙ G k
48 1 4 8 9 18 22 28 hgmapvv φ u O E k B v O E l B G G l = l
49 48 oveq1d φ u O E k B v O E l B G G l × ˙ G k = l × ˙ G k
50 47 49 eqtrd φ u O E k B v O E l B G k × ˙ G l = l × ˙ G k
51 eqid - U = - U
52 1 2 3 4 5 6 51 7 8 9 14 15 17 18 22 41 43 27 27 hdmapglem5 φ u O E k B v O E l B G S v u = S u v
53 50 52 oveq12d φ u O E k B v O E l B G k × ˙ G l ˙ G S v u = l × ˙ G k ˙ S u v
54 46 53 eqtrd φ u O E k B v O E l B G k × ˙ G l ˙ S v u = l × ˙ G k ˙ S u v
55 13 ad2antrr φ u O E k B v O E l B X V
56 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 43 41 28 27 hdmapglem7b φ u O E k B v O E l B S l · ˙ E + ˙ v k · ˙ E + ˙ u = k × ˙ G l ˙ S v u
57 56 fveq2d φ u O E k B v O E l B G S l · ˙ E + ˙ v k · ˙ E + ˙ u = G k × ˙ G l ˙ S v u
58 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 41 43 27 28 hdmapglem7b φ u O E k B v O E l B S k · ˙ E + ˙ u l · ˙ E + ˙ v = l × ˙ G k ˙ S u v
59 54 57 58 3eqtr4d φ u O E k B v O E l B G S l · ˙ E + ˙ v k · ˙ E + ˙ u = S k · ˙ E + ˙ u l · ˙ E + ˙ v
60 59 3adantl3 φ u O E k B X = k · ˙ E + ˙ u v O E l B G S l · ˙ E + ˙ v k · ˙ E + ˙ u = S k · ˙ E + ˙ u l · ˙ E + ˙ v
61 60 3adant3 φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S l · ˙ E + ˙ v k · ˙ E + ˙ u = S k · ˙ E + ˙ u l · ˙ E + ˙ v
62 simp3 φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v Y = l · ˙ E + ˙ v
63 62 fveq2d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v S Y = S l · ˙ E + ˙ v
64 simp13 φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v X = k · ˙ E + ˙ u
65 63 64 fveq12d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v S Y X = S l · ˙ E + ˙ v k · ˙ E + ˙ u
66 65 fveq2d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = G S l · ˙ E + ˙ v k · ˙ E + ˙ u
67 64 fveq2d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v S X = S k · ˙ E + ˙ u
68 67 62 fveq12d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v S X Y = S k · ˙ E + ˙ u l · ˙ E + ˙ v
69 61 66 68 3eqtr4d φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = S X Y
70 69 3exp φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = S X Y
71 70 rexlimdvv φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = S X Y
72 71 3exp φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = S X Y
73 72 rexlimdvv φ u O E k B X = k · ˙ E + ˙ u v O E l B Y = l · ˙ E + ˙ v G S Y X = S X Y
74 20 21 73 mp2d φ G S Y X = S X Y