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 ‘ 𝐴 ) ∧ 𝑣 = 𝑢 ) )