Metamath Proof Explorer

Theorem mapdpglem30

Description: Lemma for mapdpg . Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 , using lvecindp2 ) that v = 1 and v = u...". TODO: would it be shorter to have only the v = ( 1rA ) part and use mapdpglem28.u2 in mapdpglem31 ? (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
mapdpgem25.h1 ⊢ ( 𝜑 → ( ℎ ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
mapdpgem25.i1 ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ) ) )
mapdpglem26.a ⊢ 𝐴 = ( Scalar ‘ 𝑈 )
mapdpglem26.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mapdpglem26.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
mapdpglem26.o ⊢ 𝑂 = ( 0g ‘ 𝐴 )
mapdpglem28.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝐵 )
mapdpglem28.u1 ⊢ ( 𝜑 → ℎ = ( 𝑢 · 𝑖 ) )
mapdpglem28.u2 ⊢ ( 𝜑 → ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) )
mapdpglem28.ue ⊢ ( 𝜑 → 𝑢 ∈ 𝐵 )
Assertion mapdpglem30 ( 𝜑 → ( 𝑣 = ( 1r ‘ 𝐴 ) ∧ 𝑣 = 𝑢 ) )

Proof

Step Hyp Ref Expression
1 mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
6 mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
10 mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
11 mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
12 mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14 mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
15 mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
16 mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17 mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
18 mapdpgem25.h1 ⊢ ( 𝜑 → ( ℎ ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
19 mapdpgem25.i1 ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐹 ∧ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 𝑖 ) } ) ) ) )
20 mapdpglem26.a ⊢ 𝐴 = ( Scalar ‘ 𝑈 )
21 mapdpglem26.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
22 mapdpglem26.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
23 mapdpglem26.o ⊢ 𝑂 = ( 0g ‘ 𝐴 )
24 mapdpglem28.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝐵 )
25 mapdpglem28.u1 ⊢ ( 𝜑 → ℎ = ( 𝑢 · 𝑖 ) )
26 mapdpglem28.u2 ⊢ ( 𝜑 → ( 𝐺 𝑅 ℎ ) = ( 𝑣 · ( 𝐺 𝑅 𝑖 ) ) )
27 mapdpglem28.ue ⊢ ( 𝜑 → 𝑢 ∈ 𝐵 )
28 eqid ⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
29 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
30 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
31 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
32 1 8 12 lcdlvec ⊢ ( 𝜑 → 𝐶 ∈ LVec )
33 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 mapdpglem30a ⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝐶 ) )
34 eldifsn ⊢ ( 𝐺 ∈ ( 𝐹 ∖ { ( 0g ‘ 𝐶 ) } ) ↔ ( 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 0g ‘ 𝐶 ) ) )
35 15 33 34 sylanbrc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐹 ∖ { ( 0g ‘ 𝐶 ) } ) )
36 19 simpld ⊢ ( 𝜑 → 𝑖 ∈ 𝐹 )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdpglem30b ⊢ ( 𝜑 → 𝑖 ≠ ( 0g ‘ 𝐶 ) )
38 eldifsn ⊢ ( 𝑖 ∈ ( 𝐹 ∖ { ( 0g ‘ 𝐶 ) } ) ↔ ( 𝑖 ∈ 𝐹 ∧ 𝑖 ≠ ( 0g ‘ 𝐶 ) ) )
39 36 37 38 sylanbrc ⊢ ( 𝜑 → 𝑖 ∈ ( 𝐹 ∖ { ( 0g ‘ 𝐶 ) } ) )
40 1 3 20 21 8 29 30 12 lcdsbase ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝐵 )
41 24 40 eleqtrrd ⊢ ( 𝜑 → 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
42 1 3 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
43 20 lmodring ⊢ ( 𝑈 ∈ LMod → 𝐴 ∈ Ring )
44 42 43 syl ⊢ ( 𝜑 → 𝐴 ∈ Ring )
45 ringgrp ⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Grp )
46 44 45 syl ⊢ ( 𝜑 → 𝐴 ∈ Grp )
47 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
48 21 47 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
49 44 48 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
50 eqid ⊢ ( invg ‘ 𝐴 ) = ( invg ‘ 𝐴 )
51 21 50 grpinvcl ⊢ ( ( 𝐴 ∈ Grp ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
52 46 49 51 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
53 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
54 21 53 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑣 ∈ 𝐵 ∧ ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ) → ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ 𝐵 )
55 44 24 52 54 syl3anc ⊢ ( 𝜑 → ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ 𝐵 )
56 55 40 eleqtrrd ⊢ ( 𝜑 → ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
57 49 40 eleqtrrd ⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
58 21 53 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑢 ∈ 𝐵 ∧ ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ) → ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ 𝐵 )
59 44 27 52 58 syl3anc ⊢ ( 𝜑 → ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ 𝐵 )
60 59 40 eleqtrrd ⊢ ( 𝜑 → ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
61 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 mapdpglem29 ⊢ ( 𝜑 → ( 𝐽 ‘ { 𝐺 } ) ≠ ( 𝐽 ‘ { 𝑖 } ) )
62 1 3 20 21 53 8 9 22 12 52 27 36 lcdvsass ⊢ ( 𝜑 → ( ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) = ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑢 · 𝑖 ) ) )
63 62 oveq2d ⊢ ( 𝜑 → ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) ( +g ‘ 𝐶 ) ( ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) ) = ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) ( +g ‘ 𝐶 ) ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑢 · 𝑖 ) ) ) )
64 1 3 20 21 8 9 22 12 49 15 lcdvscl ⊢ ( 𝜑 → ( ( 1r ‘ 𝐴 ) · 𝐺 ) ∈ 𝐹 )
65 1 3 20 21 8 9 22 12 27 36 lcdvscl ⊢ ( 𝜑 → ( 𝑢 · 𝑖 ) ∈ 𝐹 )
66 1 3 20 50 47 8 9 28 22 10 12 64 65 lcdvsub ⊢ ( 𝜑 → ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) 𝑅 ( 𝑢 · 𝑖 ) ) = ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) ( +g ‘ 𝐶 ) ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑢 · 𝑖 ) ) ) )
67 1 3 20 21 53 8 9 22 12 52 24 36 lcdvsass ⊢ ( 𝜑 → ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) = ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑣 · 𝑖 ) ) )
68 67 oveq2d ⊢ ( 𝜑 → ( ( 𝑣 · 𝐺 ) ( +g ‘ 𝐶 ) ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) ) = ( ( 𝑣 · 𝐺 ) ( +g ‘ 𝐶 ) ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑣 · 𝑖 ) ) ) )
69 1 3 20 21 8 9 22 12 24 15 lcdvscl ⊢ ( 𝜑 → ( 𝑣 · 𝐺 ) ∈ 𝐹 )
70 1 3 20 21 8 9 22 12 24 36 lcdvscl ⊢ ( 𝜑 → ( 𝑣 · 𝑖 ) ∈ 𝐹 )
71 1 3 20 50 47 8 9 28 22 10 12 69 70 lcdvsub ⊢ ( 𝜑 → ( ( 𝑣 · 𝐺 ) 𝑅 ( 𝑣 · 𝑖 ) ) = ( ( 𝑣 · 𝐺 ) ( +g ‘ 𝐶 ) ( ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑣 · 𝑖 ) ) ) )
72 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 mapdpglem28 ⊢ ( 𝜑 → ( ( 𝑣 · 𝐺 ) 𝑅 ( 𝑣 · 𝑖 ) ) = ( 𝐺 𝑅 ( 𝑢 · 𝑖 ) ) )
73 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ ( Scalar ‘ 𝐶 ) )
74 1 3 20 47 8 29 73 12 lcd1 ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝐶 ) ) = ( 1r ‘ 𝐴 ) )
75 74 oveq1d ⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = ( ( 1r ‘ 𝐴 ) · 𝐺 ) )
76 1 8 12 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
77 9 29 22 73 lmodvs1 ⊢ ( ( 𝐶 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 1r ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝐺 )
78 76 15 77 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝐺 )
79 75 78 eqtr3d ⊢ ( 𝜑 → ( ( 1r ‘ 𝐴 ) · 𝐺 ) = 𝐺 )
80 79 oveq1d ⊢ ( 𝜑 → ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) 𝑅 ( 𝑢 · 𝑖 ) ) = ( 𝐺 𝑅 ( 𝑢 · 𝑖 ) ) )
81 72 80 eqtr4d ⊢ ( 𝜑 → ( ( 𝑣 · 𝐺 ) 𝑅 ( 𝑣 · 𝑖 ) ) = ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) 𝑅 ( 𝑢 · 𝑖 ) ) )
82 68 71 81 3eqtr2rd ⊢ ( 𝜑 → ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) 𝑅 ( 𝑢 · 𝑖 ) ) = ( ( 𝑣 · 𝐺 ) ( +g ‘ 𝐶 ) ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) ) )
83 63 66 82 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝑣 · 𝐺 ) ( +g ‘ 𝐶 ) ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) ) = ( ( ( 1r ‘ 𝐴 ) · 𝐺 ) ( +g ‘ 𝐶 ) ( ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) · 𝑖 ) ) )
84 9 28 29 30 22 31 11 32 35 39 41 56 57 60 61 83 lvecindp2 ⊢ ( 𝜑 → ( 𝑣 = ( 1r ‘ 𝐴 ) ∧ ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ) )
85 21 53 47 50 44 24 ringnegr ⊢ ( 𝜑 → ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( ( invg ‘ 𝐴 ) ‘ 𝑣 ) )
86 21 53 47 50 44 27 ringnegr ⊢ ( 𝜑 → ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( ( invg ‘ 𝐴 ) ‘ 𝑢 ) )
87 85 86 eqeq12d ⊢ ( 𝜑 → ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ↔ ( ( invg ‘ 𝐴 ) ‘ 𝑣 ) = ( ( invg ‘ 𝐴 ) ‘ 𝑢 ) ) )
88 21 50 46 24 27 grpinv11 ⊢ ( 𝜑 → ( ( ( invg ‘ 𝐴 ) ‘ 𝑣 ) = ( ( invg ‘ 𝐴 ) ‘ 𝑢 ) ↔ 𝑣 = 𝑢 ) )
89 87 88 bitrd ⊢ ( 𝜑 → ( ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ↔ 𝑣 = 𝑢 ) )
90 89 anbi2d ⊢ ( 𝜑 → ( ( 𝑣 = ( 1r ‘ 𝐴 ) ∧ ( 𝑣 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) = ( 𝑢 ( .r ‘ 𝐴 ) ( ( invg ‘ 𝐴 ) ‘ ( 1r ‘ 𝐴 ) ) ) ) ↔ ( 𝑣 = ( 1r ‘ 𝐴 ) ∧ 𝑣 = 𝑢 ) ) )
91 84 90 mpbid ⊢ ( 𝜑 → ( 𝑣 = ( 1r ‘ 𝐴 ) ∧ 𝑣 = 𝑢 ) )