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 𝐻 = ( LHyp ‘ 𝐾 )
hdmapglem7.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapglem7.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.v 𝑉 = ( Base ‘ 𝑈 )
hdmapglem7.p + = ( +g𝑈 )
hdmapglem7.q · = ( ·𝑠𝑈 )
hdmapglem7.r 𝑅 = ( Scalar ‘ 𝑈 )
hdmapglem7.b 𝐵 = ( Base ‘ 𝑅 )
hdmapglem7.a = ( LSSum ‘ 𝑈 )
hdmapglem7.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmapglem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmapglem7.x ( 𝜑𝑋𝑉 )
hdmapglem7.t × = ( .r𝑅 )
hdmapglem7.z 0 = ( 0g𝑅 )
hdmapglem7.c = ( +g𝑅 )
hdmapglem7.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.y ( 𝜑𝑌𝑉 )
Assertion hdmapglem7 ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 hdmapglem7.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapglem7.e 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapglem7.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapglem7.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapglem7.v 𝑉 = ( Base ‘ 𝑈 )
6 hdmapglem7.p + = ( +g𝑈 )
7 hdmapglem7.q · = ( ·𝑠𝑈 )
8 hdmapglem7.r 𝑅 = ( Scalar ‘ 𝑈 )
9 hdmapglem7.b 𝐵 = ( Base ‘ 𝑅 )
10 hdmapglem7.a = ( LSSum ‘ 𝑈 )
11 hdmapglem7.n 𝑁 = ( LSpan ‘ 𝑈 )
12 hdmapglem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
13 hdmapglem7.x ( 𝜑𝑋𝑉 )
14 hdmapglem7.t × = ( .r𝑅 )
15 hdmapglem7.z 0 = ( 0g𝑅 )
16 hdmapglem7.c = ( +g𝑅 )
17 hdmapglem7.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
18 hdmapglem7.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
19 hdmapglem7.y ( 𝜑𝑌𝑉 )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 hdmapglem7a ( 𝜑 → ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 19 hdmapglem7a ( 𝜑 → ∃ 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑙𝐵 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) )
22 12 ad2antrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 1 4 12 dvhlmod ( 𝜑𝑈 ∈ LMod )
24 8 lmodring ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
25 23 24 syl ( 𝜑𝑅 ∈ Ring )
26 25 ad2antrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑅 ∈ Ring )
27 simplrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑘𝐵 )
28 simprr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑙𝐵 )
29 1 4 8 9 18 22 28 hgmapcl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺𝑙 ) ∈ 𝐵 )
30 9 14 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑘𝐵 ∧ ( 𝐺𝑙 ) ∈ 𝐵 ) → ( 𝑘 × ( 𝐺𝑙 ) ) ∈ 𝐵 )
31 26 27 29 30 syl3anc ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝑘 × ( 𝐺𝑙 ) ) ∈ 𝐵 )
32 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
34 eqid ( 0g𝑈 ) = ( 0g𝑈 )
35 1 32 33 4 5 34 2 12 dvheveccl ( 𝜑𝐸 ∈ ( 𝑉 ∖ { ( 0g𝑈 ) } ) )
36 35 eldifad ( 𝜑𝐸𝑉 )
37 36 snssd ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
38 1 4 5 3 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
39 12 37 38 syl2anc ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
40 39 ad2antrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
41 simplrl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) )
42 40 41 sseldd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑢𝑉 )
43 simprl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) )
44 40 43 sseldd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑣𝑉 )
45 1 4 5 8 9 17 22 42 44 hdmapipcl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( ( 𝑆𝑣 ) ‘ 𝑢 ) ∈ 𝐵 )
46 1 4 8 9 16 18 22 31 45 hgmapadd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑘 × ( 𝐺𝑙 ) ) ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) ) = ( ( 𝐺 ‘ ( 𝑘 × ( 𝐺𝑙 ) ) ) ( 𝐺 ‘ ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) ) )
47 1 4 8 9 14 18 22 27 29 hgmapmul ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( 𝑘 × ( 𝐺𝑙 ) ) ) = ( ( 𝐺 ‘ ( 𝐺𝑙 ) ) × ( 𝐺𝑘 ) ) )
48 1 4 8 9 18 22 28 hgmapvv ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( 𝐺𝑙 ) ) = 𝑙 )
49 48 oveq1d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( ( 𝐺 ‘ ( 𝐺𝑙 ) ) × ( 𝐺𝑘 ) ) = ( 𝑙 × ( 𝐺𝑘 ) ) )
50 47 49 eqtrd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( 𝑘 × ( 𝐺𝑙 ) ) ) = ( 𝑙 × ( 𝐺𝑘 ) ) )
51 eqid ( -g𝑈 ) = ( -g𝑈 )
52 1 2 3 4 5 6 51 7 8 9 14 15 17 18 22 41 43 27 27 hdmapglem5 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) = ( ( 𝑆𝑢 ) ‘ 𝑣 ) )
53 50 52 oveq12d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( ( 𝐺 ‘ ( 𝑘 × ( 𝐺𝑙 ) ) ) ( 𝐺 ‘ ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) ) = ( ( 𝑙 × ( 𝐺𝑘 ) ) ( ( 𝑆𝑢 ) ‘ 𝑣 ) ) )
54 46 53 eqtrd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑘 × ( 𝐺𝑙 ) ) ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) ) = ( ( 𝑙 × ( 𝐺𝑘 ) ) ( ( 𝑆𝑢 ) ‘ 𝑣 ) ) )
55 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → 𝑋𝑉 )
56 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 43 41 28 27 hdmapglem7b ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) = ( ( 𝑘 × ( 𝐺𝑙 ) ) ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) )
57 56 fveq2d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ) = ( 𝐺 ‘ ( ( 𝑘 × ( 𝐺𝑙 ) ) ( ( 𝑆𝑣 ) ‘ 𝑢 ) ) ) )
58 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 41 43 27 28 hdmapglem7b ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) = ( ( 𝑙 × ( 𝐺𝑘 ) ) ( ( 𝑆𝑢 ) ‘ 𝑣 ) ) )
59 54 57 58 3eqtr4d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ) = ( ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) )
60 59 3adantl3 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ) → ( 𝐺 ‘ ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ) = ( ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) )
61 60 3adant3 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( 𝐺 ‘ ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ) = ( ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) )
62 simp3 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) )
63 62 fveq2d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( 𝑆𝑌 ) = ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) )
64 simp13 ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
65 63 64 fveq12d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( ( 𝑆𝑌 ) ‘ 𝑋 ) = ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
66 65 fveq2d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( 𝐺 ‘ ( ( 𝑆 ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ) )
67 64 fveq2d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( 𝑆𝑋 ) = ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
68 67 62 fveq12d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( ( 𝑆𝑋 ) ‘ 𝑌 ) = ( ( 𝑆 ‘ ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ‘ ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) )
69 61 66 68 3eqtr4d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) ∧ ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) ∧ 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) )
70 69 3exp ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) → ( ( 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑙𝐵 ) → ( 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) ) ) )
71 70 rexlimdvv ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) ∧ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) → ( ∃ 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑙𝐵 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) ) )
72 71 3exp ( 𝜑 → ( ( 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘𝐵 ) → ( 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) → ( ∃ 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑙𝐵 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) ) ) ) )
73 72 rexlimdvv ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) → ( ∃ 𝑣 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑙𝐵 𝑌 = ( ( 𝑙 · 𝐸 ) + 𝑣 ) → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) ) ) )
74 20 21 73 mp2d ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆𝑋 ) ‘ 𝑌 ) )