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 ⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) )